![]() |
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 113 | . 2 ⊢ (φ → ψ) |
4 | 1, 3 | ax-mp 7 | 1 ⊢ ψ |
Colors of variables: wff set class |
Syntax hints: ↔ wb 98 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: pm5.74i 169 pm4.71i 371 pm4.71ri 372 pm5.32i 427 pm3.24 626 olc 631 orc 632 dn1dc 866 3ori 1194 mpto2 1312 mtp-xor 1313 mpgbi 1338 dveeq2 1693 dveeq2or 1694 sbequilem 1716 nfsb 1819 sbco 1839 sbcocom 1841 elsb3 1849 elsb4 1850 hbsbd 1855 dvelimALT 1883 dvelimfv 1884 dvelimor 1891 eqcomi 2041 eqtri 2057 eleqtri 2109 neii 2205 neeqtri 2226 nesymi 2245 necomi 2284 nemtbir 2288 neli 2293 nrex 2405 rexlimi 2420 isseti 2557 eueq1 2707 euxfr2dc 2720 cdeqri 2744 sseqtri 2971 3sstr3i 2977 pssn2lp 3039 equncomi 3083 unssi 3112 ssini 3154 unabs 3161 inabs 3162 ddifss 3169 inssddif 3172 rgenm 3317 snid 3394 rabrsndc 3429 rintm 3735 breqtri 3778 bm1.3ii 3869 zfnuleu 3872 zfpow 3919 copsexg 3972 uniop 3983 pwundifss 4013 onunisuci 4135 zfun 4137 op1stb 4175 op1stbg 4176 ordtriexmidlem 4208 ordtriexmid 4210 ordtri2orexmid 4211 onsucsssucexmid 4212 onsucelsucexmidlem 4214 onsucelsucexmid 4215 dtruex 4237 ordsoexmid 4240 tfi 4248 relop 4429 rn0 4531 dmresi 4604 issref 4650 cnvcnv 4716 rescnvcnv 4726 cnvcnvres 4727 cnvsn 4746 cocnvcnv2 4775 cores2 4776 co01 4778 relcoi1 4792 cnviinm 4802 fnopab 4966 mpt0 4969 fnmpti 4970 f1cnvcnv 5043 f1ovi 5108 fmpti 5264 fvsnun2 5304 oprabss 5532 2nd0 5714 f1stres 5728 f2ndres 5729 reldmtpos 5809 dftpos4 5819 tpostpos 5820 tpos0 5830 smo0 5854 frecfnom 5925 oasuc 5983 ssdomg 6194 xpcomf1o 6235 ssfiexmid 6254 dmaddpi 6309 dmmulpi 6310 1lt2pi 6324 1lt2nq 6389 gtso 6894 subf 7010 negne0i 7082 negdii 7091 neg1ap0 7804 halflt1 7919 nn0ssz 8039 zeo 8119 numlt 8162 numltc 8163 uzf 8252 indstr 8312 ixxf 8537 iooval2 8554 ioof 8610 unirnioo 8612 fzval2 8647 fzf 8648 fz10 8680 fzpreddisj 8703 4fvwrd4 8767 fzof 8771 bdceqi 9298 bdcriota 9338 bdsepnfALT 9344 bdbm1.3ii 9346 bj-d0clsepcl 9384 |
Copyright terms: Public domain | W3C validator |