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 kii 13 si 15 mpd 16 mp2 32 ge-lei 37 ge-rei 39 mp2an 50 goli 53 gori 55 go-comi 66 bi 69 naaii 80 anaiii 86 najaii 91 janaiii 97 nagihaii 102 gihanaiii 107 ge-go 111 spec1i 182 spec2i 184 qi1i 186 qi1-mp 187 qi2i 189 qi2-mp 190 lnci 214 nakuii 216 sdoi 220 efqi 222 efqii 223 gripauiis 262 ceri-lin 336 ceri-rin 337 ebi 344 eqi 346 subid 355 nfri 361 zilcmi-nomei 368 cmima-zilcmi 369 nibliii 412 zihoi 434 sezni-elt 468 baihei-inj 474 succ-succi 489 nat-indi 491 kazmi-funii 523 pagbu-antisym 529 pagbu-trans 531 fancuii 576

W3C validator