![]() |
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 118 | . 2 ⊢ (𝜑 → 𝜓) |
4 | 1, 3 | ax-mp 7 | 1 ⊢ 𝜓 |
Colors of variables: wff set class |
Syntax hints: ↔ wb 103 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: pm5.74i 178 pm4.71i 383 pm4.71ri 384 pm5.32i 442 pm3.24 660 olc 665 orc 666 dn1dc 902 3ori 1232 mptxor 1356 mpgbi 1382 dveeq2 1738 dveeq2or 1739 sbequilem 1761 nfsb 1865 sbco 1885 sbcocom 1887 elsb3 1895 elsb4 1896 hbsbd 1901 dvelimALT 1929 dvelimfv 1930 dvelimor 1937 eqcomi 2087 eqtri 2103 eleqtri 2157 neii 2251 neeqtri 2276 nesymi 2295 necomi 2334 nemtbir 2338 neli 2346 nrex 2458 rexlimi 2475 isseti 2616 eueq1 2774 euxfr2dc 2787 cdeqri 2811 sseqtri 3041 3sstr3i 3047 equncomi 3129 unssi 3158 ssini 3206 unabs 3213 inabs 3214 ddifss 3219 inssddif 3222 rgenm 3361 snid 3444 rabrsndc 3479 rintm 3786 breqtri 3829 bm1.3ii 3920 zfnuleu 3923 zfpow 3970 undifexmid 3985 copsexg 4028 uniop 4039 pwundifss 4069 onunisuci 4216 zfun 4218 op1stb 4256 op1stbg 4257 ordtriexmidlem 4292 ordtriexmid 4294 ordtri2orexmid 4295 2ordpr 4296 ontr2exmid 4297 onsucsssucexmid 4299 onsucelsucexmid 4302 dtruex 4331 ordsoexmid 4334 0elsucexmid 4337 ordtri2or2exmid 4343 tfi 4352 relop 4535 rn0 4637 dmresi 4712 issref 4758 cnvcnv 4824 rescnvcnv 4834 cnvcnvres 4835 cnvsn 4854 cocnvcnv2 4883 cores2 4884 co01 4886 relcoi1 4900 cnviinm 4910 fnopab 5075 mpt0 5078 fnmpti 5079 f1cnvcnv 5152 f1ovi 5217 fmpti 5374 fvsnun2 5414 oprabss 5642 2nd0 5824 f1stres 5838 f2ndres 5839 reldmtpos 5923 dftpos4 5933 tpostpos 5934 tpos0 5944 smo0 5968 frecfnom 6071 oasuc 6129 ssdomg 6347 xpcomf1o 6391 ssfilem 6432 diffitest 6444 inffiexmid 6458 card0 6552 dmaddpi 6613 dmmulpi 6614 1lt2pi 6628 1lt2nq 6694 gtso 7293 subf 7413 negne0i 7486 negdii 7495 ltapii 7836 neg1ap0 8251 halflt1 8351 nn0ssz 8486 3halfnz 8561 zeo 8569 numlt 8618 numltc 8619 le9lt10 8620 decle 8627 uzf 8739 indstr 8798 infrenegsupex 8799 ixxf 9033 iooval2 9050 ioof 9106 unirnioo 9108 fzval2 9144 fzf 9145 fz10 9177 fzpreddisj 9200 4fvwrd4 9263 fzof 9267 fldiv4p1lem1div2 9423 sqrt2gt1lt2 10120 fclim 10318 n2dvds1 10503 flodddiv4 10525 gcdf 10555 eucalgf 10628 2prm 10700 dfphi2 10787 znnen 10802 ex-fl 10807 bdceqi 10885 bdcriota 10925 bdsepnfALT 10931 bdbm1.3ii 10933 bj-d0clsepcl 10971 |
Copyright terms: Public domain | W3C validator |