![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mpbi | GIF version |
Description: An inference from a biconditional, related to modus ponens. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
mpbi.min | ⊢ 𝜑 |
mpbi.maj | ⊢ (𝜑 ↔ 𝜓) |
Ref | Expression |
---|---|
mpbi | ⊢ 𝜓 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpbi.min | . 2 ⊢ 𝜑 | |
2 | mpbi.maj | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
3 | 2 | biimpi 119 | . 2 ⊢ (𝜑 → 𝜓) |
4 | 1, 3 | ax-mp 7 | 1 ⊢ 𝜓 |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: pm5.74i 179 pm4.71i 386 pm4.71ri 387 pm5.32i 447 biadanii 585 pm3.24 665 olc 683 orc 684 dcnn 816 dn1dc 927 3ori 1261 mptxor 1385 mpgbi 1411 dveeq2 1769 dveeq2or 1770 sbequilem 1792 nfsb 1897 sbco 1917 sbcocom 1919 elsb3 1927 elsb4 1928 hbsbd 1933 dvelimALT 1961 dvelimfv 1962 dvelimor 1969 eqcomi 2119 eqtri 2135 eleqtri 2189 neii 2284 neeqtri 2309 nesymi 2328 necomi 2367 nemtbir 2371 neli 2379 nrex 2498 rexlimi 2516 isseti 2665 eueq1 2825 euxfr2dc 2838 cdeqri 2864 sseqtri 3097 3sstr3i 3103 equncomi 3188 unssi 3217 ssini 3265 unabs 3273 inabs 3274 ddifss 3280 inssddif 3283 rgenm 3431 snid 3522 rabrsndc 3557 rintm 3871 breqtri 3918 bm1.3ii 4009 zfnuleu 4012 zfpow 4059 undifexmid 4077 copsexg 4126 uniop 4137 pwundifss 4167 onunisuci 4314 zfun 4316 op1stb 4359 op1stbg 4360 ordtriexmidlem 4395 ordtriexmid 4397 ordtri2orexmid 4398 2ordpr 4399 ontr2exmid 4400 onsucsssucexmid 4402 onsucelsucexmid 4405 dtruex 4434 ordsoexmid 4437 0elsucexmid 4440 ordtri2or2exmid 4446 dcextest 4455 tfi 4456 relop 4649 dmxpid 4720 rn0 4753 dmresi 4832 issref 4879 cnvcnv 4949 rescnvcnv 4959 cnvcnvres 4960 cnvsn 4979 cocnvcnv2 5008 cores2 5009 co01 5011 relcoi1 5028 cnviinm 5038 fnopab 5205 mpt0 5208 fnmpti 5209 f1cnvcnv 5297 f1ovi 5362 fmpti 5526 fvsnun2 5572 oprabss 5811 2nd0 5997 f1stres 6011 f2ndres 6012 reldmtpos 6104 dftpos4 6114 tpostpos 6115 tpos0 6125 smo0 6149 frecfnom 6252 oasuc 6314 uniixp 6569 ssdomg 6626 xpcomf1o 6672 ssfilem 6722 diffitest 6734 inffiexmid 6753 fiintim 6770 caseinl 6928 caseinr 6929 eninl 6934 eninr 6935 card0 6994 dju1p1e2 7001 dmaddpi 7081 dmmulpi 7082 1lt2pi 7096 1lt2nq 7162 gtso 7766 subf 7887 negne0i 7960 negdii 7969 ltapii 8314 sup3exmid 8625 neg1ap0 8739 halflt1 8841 nn0ssz 8976 3halfnz 9052 zeo 9060 numlt 9110 numltc 9111 le9lt10 9112 decle 9119 uzf 9231 indstr 9290 infrenegsupex 9291 xaddf 9520 ixxf 9574 iooval2 9591 ioof 9647 unirnioo 9649 fzval2 9686 fzf 9687 fz10 9719 fzpreddisj 9744 4fvwrd4 9810 fzof 9814 fldiv4p1lem1div2 9971 sqrt2gt1lt2 10713 infxrnegsupex 10924 fclim 10955 fsumrelem 11132 arisum2 11160 geo2sum2 11176 0.999... 11182 ege2le3 11228 sin0 11287 ef01bndlem 11314 cos2bnd 11318 cos01gt0 11320 sincos2sgn 11323 sin4lt0 11324 egt2lt3 11334 n2dvds1 11457 flodddiv4 11479 gcdf 11509 eucalgf 11582 2prm 11654 dfphi2 11741 znnen 11756 ennnfonelem1 11765 qnnen 11789 ctiunct 11796 structcnvcnv 11818 structfn 11821 eltpsi 12051 unitg 12074 epttop 12102 txuni2 12267 retopon 12515 reldvg 12603 ex-fl 12630 ex-exp 12632 bdceqi 12731 bdcriota 12771 bdsepnfALT 12777 bdbm1.3ii 12779 bj-d0clsepcl 12813 nninfsellemeqinf 12902 |
Copyright terms: Public domain | W3C validator |