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 269 lnci 276 nakuii 278 sdoi 282 efqi 285 efqii 287 nakunakui 294 gripauiis 336 ceri-lin 410 ceri-rin 411 ebi 419 eqi 421 nfri 439 subid 452 zilcmi-nomei 461 cmima-zilcmi 462 nibliii 508 zihoi 530 sezni-elt 571 baihei-inj 578 succ-succi 593 nat-indi 595 kazmi-funii 627 pagbu-antisym 633 pagbu-trans 635 fancuii 704

W3C validator