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 8313 1ap0 8320 sup3exmid 8683 nn1suc 8707 neg1lt0 8796 4d2e2 8848 iap0 8911 un0mulcl 8979 pnf0xnn0 9015 3halfnz 9116 nummac 9194 uzf 9297 mnfltpnf 9539 ixxf 9649 ioof 9722 fzf 9762 fzp1disj 9828 fzp1nel 9852 fzo0 9913 frecfzennn 10167 frechashgf1o 10169 fxnn0nninf 10179 seq3f1olemp 10243 sq0 10351 irec 10360 hash0 10511 prhash2ex 10523 climmo 11035 sum0 11125 fisumcom2 11175 cos1bnd 11393 cos2bnd 11394 n2dvdsm1 11537 n2dvds3 11539 flodddiv4 11558 3lcm2e6woprm 11694 6lcm4e12 11695 2prm 11735 3lcm2e6 11765 unennn 11837 structcnvcnv 11902 strleun 11975 restid 12058 tgdom 12168 tgidm 12170 resttopon 12267 rest0 12275 psmetrel 12418 metrel 12438 xmetrel 12439 xmetf 12446 0met 12480 mopnrel 12537 setsmsbasg 12575 setsmsdsg 12576 qtopbasss 12617 reldvg 12744 dvexp 12771 dveflem 12782 efcn 12784 sinhalfpilem 12799 sincosq1lem 12833 tangtx 12846 sincos4thpi 12848 pigt3 12852 ex-fl 12864 bj-nndcALT 12890 bj-axempty 13018 bj-axempty2 13019 bdinex1 13024 bj-zfpair2 13035 bj-uniex2 13041 bj-indint 13056 bj-omind 13059 bj-omex 13067 bj-omelon 13086 pw1dom2 13117 0nninf 13124 |
Copyright terms: Public domain | W3C validator |