Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mpbir | Unicode 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 132 | . 2 |
4 | 1, 3 | ax-mp 5 | 1 |
Colors of variables: wff set class |
Syntax hints: wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: pm5.74ri 180 imnani 665 stabnot 803 mpbir2an 911 mpbir3an 1148 tru 1320 mpgbir 1414 nfxfr 1435 19.8a 1554 sbt 1742 dveeq2 1771 dveeq2or 1772 sbequilem 1794 cbvex2 1874 dvelimALT 1963 dvelimfv 1964 dvelimor 1971 nfeuv 1995 moaneu 2053 moanmo 2054 eqeltri 2190 nfcxfr 2255 neir 2288 neirr 2294 eqnetri 2308 nesymir 2332 nelir 2383 mprgbir 2467 vex 2663 issetri 2669 moeq 2832 cdeqi 2867 ru 2881 eqsstri 3099 3sstr4i 3108 rgenm 3435 mosn 3530 rabrsndc 3561 tpid1 3604 tpid2 3606 tpid3 3609 pwv 3705 uni0 3733 eqbrtri 3919 tr0 4007 trv 4008 zfnuleu 4022 0ex 4025 inex1 4032 0elpw 4058 axpow2 4070 axpow3 4071 vpwex 4073 zfpair2 4102 exss 4119 moop2 4143 pwundifss 4177 po0 4203 epse 4234 fr0 4243 0elon 4284 onm 4293 uniex2 4328 snnex 4339 ordtriexmidlem 4405 ordtriexmid 4407 ontr2exmid 4410 ordtri2or2exmidlem 4411 onsucsssucexmid 4412 onsucelsucexmidlem 4414 ruALT 4436 zfregfr 4458 dcextest 4465 zfinf2 4473 omex 4477 finds 4484 finds2 4485 ordom 4490 omsinds 4505 relsnop 4615 relxp 4618 rel0 4634 relopabi 4635 eliunxp 4648 opeliunxp2 4649 dmi 4724 xpidtr 4899 cnvcnv 4961 dmsn0 4976 cnvsn0 4977 funmpt 5131 funmpt2 5132 funinsn 5142 isarep2 5180 f0 5283 f10 5369 f1o00 5370 f1oi 5373 f1osn 5375 brprcneu 5382 fvopab3ig 5463 opabex 5612 eufnfv 5616 mpofun 5841 reldmmpo 5850 ovid 5855 ovidig 5856 ovidi 5857 ovig 5860 ovi3 5875 oprabex 5994 oprabex3 5995 f1stres 6025 f2ndres 6026 opeliunxp2f 6103 tpos0 6139 issmo 6153 tfrlem6 6181 tfrlem8 6183 tfri1dALT 6216 tfrcl 6229 rdgfun 6238 frecfun 6260 frecfcllem 6269 0lt1o 6305 eqer 6429 ecopover 6495 ecopoverg 6498 th3qcor 6501 mapsnf1o3 6559 ssdomg 6640 ensn1 6658 xpcomf1o 6687 fiunsnnn 6743 finexdc 6764 exmidpw 6770 omct 6970 infnninf 6990 nnnninf 6991 pm54.43 7014 exmidonfinlem 7017 dmaddpi 7101 dmmulpi 7102 1lt2pi 7116 indpi 7118 1lt2nq 7182 genpelxp 7287 ltexprlempr 7384 recexprlempr 7408 cauappcvgprlemcl 7429 cauappcvgprlemladd 7434 caucvgprlemcl 7452 caucvgprprlemcl 7480 m1p1sr 7536 m1m1sr 7537 0lt1sr 7541 peano1nnnn 7628 ax1cn 7637 ax1re 7638 axaddf 7644 axmulf 7645 ax0lt1 7652 0lt1 7857 subaddrii 8019 ixi 8312 1ap0 8319 sup3exmid 8679 nn1suc 8703 neg1lt0 8792 4d2e2 8838 iap0 8901 un0mulcl 8969 pnf0xnn0 9005 3halfnz 9106 nummac 9184 uzf 9285 mnfltpnf 9526 ixxf 9636 ioof 9709 fzf 9749 fzp1disj 9815 fzp1nel 9839 fzo0 9900 frecfzennn 10154 frechashgf1o 10156 fxnn0nninf 10166 seq3f1olemp 10230 sq0 10338 irec 10347 hash0 10498 prhash2ex 10510 climmo 11022 sum0 11112 fisumcom2 11162 cos1bnd 11380 cos2bnd 11381 n2dvdsm1 11522 n2dvds3 11524 flodddiv4 11543 3lcm2e6woprm 11679 6lcm4e12 11680 2prm 11720 3lcm2e6 11750 unennn 11821 structcnvcnv 11886 strleun 11959 restid 12042 tgdom 12152 tgidm 12154 resttopon 12251 rest0 12259 psmetrel 12402 metrel 12422 xmetrel 12423 xmetf 12430 0met 12464 mopnrel 12521 setsmsbasg 12559 setsmsdsg 12560 qtopbasss 12601 reldvg 12728 dvexp 12755 dveflem 12766 efcn 12768 sinhalfpilem 12783 sincosq1lem 12817 ex-fl 12833 bj-nndcALT 12859 bj-axempty 12987 bj-axempty2 12988 bdinex1 12993 bj-zfpair2 13004 bj-uniex2 13010 bj-indint 13025 bj-omind 13028 bj-omex 13036 bj-omelon 13055 pw1dom2 13086 0nninf 13093 |
Copyright terms: Public domain | W3C validator |