![]() |
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: ![]() |
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 681 stabnot 819 mpbir2an 927 mpbir3an 1164 tru 1336 mpgbir 1430 nfxfr 1451 19.8a 1570 sbt 1758 dveeq2 1788 dveeq2or 1789 sbequilem 1811 cbvex2 1895 dvelimALT 1986 dvelimfv 1987 dvelimor 1994 nfeuv 2018 moaneu 2076 moanmo 2077 eqeltri 2213 nfcxfr 2279 neir 2312 neirr 2318 eqnetri 2332 nesymir 2356 nelir 2407 mprgbir 2493 vex 2692 issetri 2698 moeq 2863 cdeqi 2898 ru 2912 eqsstri 3134 3sstr4i 3143 rgenm 3470 mosn 3567 rabrsndc 3599 tpid1 3642 tpid2 3644 tpid3 3647 pwv 3743 uni0 3771 eqbrtri 3957 tr0 4045 trv 4046 zfnuleu 4060 0ex 4063 inex1 4070 0elpw 4096 axpow2 4108 axpow3 4109 vpwex 4111 zfpair2 4140 exss 4157 moop2 4181 pwundifss 4215 po0 4241 epse 4272 fr0 4281 0elon 4322 onm 4331 uniex2 4366 snnex 4377 ordtriexmidlem 4443 ordtriexmid 4445 ontr2exmid 4448 ordtri2or2exmidlem 4449 onsucsssucexmid 4450 onsucelsucexmidlem 4452 ruALT 4474 zfregfr 4496 dcextest 4503 zfinf2 4511 omex 4515 finds 4522 finds2 4523 ordom 4528 omsinds 4543 relsnop 4653 relxp 4656 rel0 4672 relopabi 4673 eliunxp 4686 opeliunxp2 4687 dmi 4762 xpidtr 4937 cnvcnv 4999 dmsn0 5014 cnvsn0 5015 funmpt 5169 funmpt2 5170 funinsn 5180 isarep2 5218 f0 5321 f10 5409 f1o00 5410 f1oi 5413 f1osn 5415 brprcneu 5422 fvopab3ig 5503 opabex 5652 eufnfv 5656 mpofun 5881 reldmmpo 5890 ovid 5895 ovidig 5896 ovidi 5897 ovig 5900 ovi3 5915 oprabex 6034 oprabex3 6035 f1stres 6065 f2ndres 6066 opeliunxp2f 6143 tpos0 6179 issmo 6193 tfrlem6 6221 tfrlem8 6223 tfri1dALT 6256 tfrcl 6269 rdgfun 6278 frecfun 6300 frecfcllem 6309 0lt1o 6345 eqer 6469 ecopover 6535 ecopoverg 6538 th3qcor 6541 mapsnf1o3 6599 ssdomg 6680 ensn1 6698 xpcomf1o 6727 fiunsnnn 6783 finexdc 6804 exmidpw 6810 omct 7010 infnninf 7030 nnnninf 7031 pm54.43 7063 exmidonfinlem 7066 dmaddpi 7157 dmmulpi 7158 1lt2pi 7172 indpi 7174 1lt2nq 7238 genpelxp 7343 ltexprlempr 7440 recexprlempr 7464 cauappcvgprlemcl 7485 cauappcvgprlemladd 7490 caucvgprlemcl 7508 caucvgprprlemcl 7536 m1p1sr 7592 m1m1sr 7593 0lt1sr 7597 peano1nnnn 7684 ax1cn 7693 ax1re 7694 axaddf 7700 axmulf 7701 ax0lt1 7708 0lt1 7913 subaddrii 8075 ixi 8369 1ap0 8376 sup3exmid 8739 nn1suc 8763 neg1lt0 8852 4d2e2 8904 iap0 8967 un0mulcl 9035 pnf0xnn0 9071 3halfnz 9172 nummac 9250 uzf 9353 mnfltpnf 9601 ixxf 9711 ioof 9784 fzf 9825 fzp1disj 9891 fzp1nel 9915 fzo0 9976 frecfzennn 10230 frechashgf1o 10232 fxnn0nninf 10242 seq3f1olemp 10306 sq0 10414 irec 10423 hash0 10575 prhash2ex 10587 climmo 11099 sum0 11189 fisumcom2 11239 cos1bnd 11502 cos2bnd 11503 n2dvdsm1 11646 n2dvds3 11648 flodddiv4 11667 3lcm2e6woprm 11803 6lcm4e12 11804 2prm 11844 3lcm2e6 11874 unennn 11946 structcnvcnv 12014 strleun 12087 restid 12170 tgdom 12280 tgidm 12282 resttopon 12379 rest0 12387 psmetrel 12530 metrel 12550 xmetrel 12551 xmetf 12558 0met 12592 mopnrel 12649 setsmsbasg 12687 setsmsdsg 12688 qtopbasss 12729 reldvg 12856 dvexp 12883 dveflem 12895 efcn 12897 sinhalfpilem 12920 sincosq1lem 12954 tangtx 12967 sincos4thpi 12969 pigt3 12973 dfrelog 12989 relogf1o 12990 log1 12995 loge 12996 relogiso 13002 2logb9irr 13096 2logb9irrap 13102 ex-fl 13108 bj-nndcALT 13134 bj-axempty 13262 bj-axempty2 13263 bdinex1 13268 bj-zfpair2 13279 bj-uniex2 13285 bj-indint 13300 bj-omind 13303 bj-omex 13311 bj-omelon 13330 pw1dom2 13361 0nninf 13372 dceqnconst 13423 |
Copyright terms: Public domain | W3C validator |