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 18 mp2 37 ge-lei 51 ge-rei 53 mp2an 75 goli 84 gori 86 go-comi 98 bi 101 naaii 112 anaiii 118 najaii 123 janaiii 129 nagihaii 134 gihanaiii 139 ge-go 143 ga-li 175 ga-ri 176 mpg1 225 spec1i 229 spec2i 233 qi1i 235 qi1-mp 236 qi2i 240 qi2-mp 241 mp-ceihi 270 lnci 277 nakuii 279 sdoi 283 efqi 286 efqii 288 nakunakui 295 gripauiis 337 ceri-lin 412 ceri-rin 413 ebi 421 eqi 423 nfri 441 subid 454 zilcmi-nomei 466 cmima-zilcmi 467 selcmi-zilcmi 468 nibliii 514 zihoi 536 sezni-elt 577 baihei-inj 584 succ-succi 599 nat-indi 601 kazmi-funii 635 pagbu-antisym 646 pagbu-trans 648 fancuii 731

W3C validator