ax-mp - brismu bridi

	brismu bridi		< Previous Next > Nearby theorems
Mirrors > Home > Home > Th. List > ax-mp

Axiom ax-mp 10

Description: Because {ganai} encodes a syllogism, it may be eliminated by modus ponens. In terms of categorical logic, {broda} implies {brode} and {broda} is assumed.

**Hypotheses**
Ref	Expression
ax-mp.0	⊢ broda
ax-mp.1	⊢ ganai broda gi brode

**Assertion**
Ref	Expression
ax-mp	⊢ brode

This axiom is referenced by: ki 12 mpki 13 kii 14 si 16 mpd 17 mp2 35 ge-lei 46 ge-rei 48 mp2an 59 goli 62 gori 64 go-comi 76 bi 79 naaii 90 anaiii 96 najaii 101 janaiii 107 nagihaii 112 gihanaiii 117 ge-go 121 ga-li 148 ga-ri 149 mpg1 194 spec1i 197 spec2i 200 qi1i 202 qi1-mp 203 qi2i 205 qi2-mp 206 mp-ceihi 233 lnci 240 nakuii 242 sdoi 246 efqi 249 efqii 251 nakunakui 257 gripauiis 299 ceri-lin 373 ceri-rin 374 ebi 382 eqi 384 subid 394 nfri 400 zilcmi-nomei 410 cmima-zilcmi 411 nibliii 454 zihoi 476 sezni-elt 510 baihei-inj 516 succ-succi 531 nat-indi 533 kazmi-funii 565 pagbu-antisym 571 pagbu-trans 573 fancuii 629

W3C validator