![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mpbir | GIF version |
Description: An inference from a biconditional, related to modus ponens. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
mpbir.min | ⊢ ψ |
mpbir.maj | ⊢ (φ ↔ ψ) |
Ref | Expression |
---|---|
mpbir | ⊢ φ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpbir.min | . 2 ⊢ ψ | |
2 | mpbir.maj | . . 3 ⊢ (φ ↔ ψ) | |
3 | 2 | biimpri 124 | . 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 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: pm5.74ri 170 imnani 624 stabnot 740 mpbir2an 848 mpbir3an 1085 tru 1246 mpto1 1311 mpgbir 1339 nfxfr 1360 19.8a 1479 sbt 1664 dveeq2 1693 dveeq2or 1694 sbequilem 1716 cbvex2 1794 dvelimALT 1883 dvelimfv 1884 dvelimor 1891 nfeuv 1915 moaneu 1973 moanmo 1974 eqeltri 2107 nfcxfr 2172 neir 2206 neirr 2210 eqnetri 2222 nesymir 2246 nelir 2294 mprgbir 2373 vex 2554 issetri 2558 moeq 2710 cdeqi 2743 ru 2757 eqsstri 2969 3sstr4i 2978 rgenm 3317 mosn 3398 rabrsndc 3429 tpid1 3472 tpid2 3473 tpid3 3475 pwv 3570 uni0 3598 eqbrtri 3774 tr0 3856 trv 3857 zfnuleu 3872 0ex 3875 inex1 3882 0elpw 3908 axpow2 3920 axpow3 3921 pwex 3923 zfpair2 3936 exss 3954 moop2 3979 pwundifss 4013 po0 4039 epse 4064 0elon 4095 onm 4104 uniex2 4139 snnex 4147 ordtriexmidlem 4208 ordtriexmid 4210 onsucsssucexmid 4212 onsucelsucexmidlem 4214 ruALT 4229 zfinf2 4255 omex 4259 finds 4266 finds2 4267 ordom 4272 relsnop 4387 relxp 4390 rel0 4405 relopabi 4406 eliunxp 4418 opeliunxp2 4419 dmi 4493 xpidtr 4658 cnvcnv 4716 dmsn0 4731 cnvsn0 4732 funmpt 4881 funmpt2 4882 isarep2 4929 f0 5023 f10 5103 f1o00 5104 f1oi 5107 f1osn 5109 brprcneu 5114 fvopab3ig 5189 opabex 5328 eufnfv 5332 mpt2fun 5545 reldmmpt2 5554 ovid 5559 ovidig 5560 ovidi 5561 ovig 5564 ovi3 5579 oprabex 5697 oprabex3 5698 f1stres 5728 f2ndres 5729 tpos0 5830 issmo 5844 tfrlem6 5873 tfrlem8 5875 rdgfun 5900 0lt1o 5962 eqer 6074 ecopover 6140 ecopoverg 6143 th3qcor 6146 ssdomg 6194 ensn1 6212 xpcomf1o 6235 dmaddpi 6309 dmmulpi 6310 1lt2pi 6324 indpi 6326 1lt2nq 6389 genpelxp 6494 ltexprlempr 6582 recexprlempr 6604 cauappcvgprlemcl 6625 cauappcvgprlemladd 6630 caucvgprlemcl 6647 m1p1sr 6688 m1m1sr 6689 0lt1sr 6693 ax1cn 6747 ax1re 6748 ax0lt1 6760 ax-0lt1 6789 0lt1 6938 subaddrii 7096 ixi 7367 1ap0 7374 nn1suc 7714 neg1lt0 7803 4d2e2 7854 iap0 7925 un0mulcl 7992 nummac 8175 uzf 8252 mnfltpnf 8476 ixxf 8537 ioof 8610 fzf 8648 fzp1disj 8712 fzp1nel 8736 fzo0 8794 frecfzennn 8884 frechashgf1o 8886 sq0 8997 irec 9005 bj-axempty 9348 bj-axempty2 9349 bdinex1 9354 bj-zfpair2 9365 bj-uniex2 9371 bj-indint 9390 bj-omind 9393 bj-omex 9402 bj-omelon 9421 |
Copyright terms: Public domain | W3C validator |