![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > mp2 | Structured version Unicode version |
Description: A double modus ponens inference. (Contributed by NM, 5-Apr-1994.) (Proof modification is discouraged.) |
Ref | Expression |
---|---|
mp2.1 |
![]() ![]() |
mp2.2 |
![]() ![]() |
mp2.3 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
mp2 |
![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mp2.2 |
. 2
![]() ![]() | |
2 | mp2.1 |
. . 3
![]() ![]() | |
3 | mp2.3 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | ax-mp 5 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | ax-mp 5 |
1
![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() |
This theorem was proved from axioms: ax-mp 5 |
This theorem is referenced by: impbii 188 imbi12i 326 pm3.2i 455 sbcom2 2160 sstri 3472 0disj 4392 disjx0 4394 relres 5245 cnvdif 5350 difxp 5369 funopab4 5560 fun0 5582 fvsn 6019 reltpos 6859 tpostpos 6874 tpos0 6884 oaabs2 7193 swoer 7238 xpider 7280 erinxp 7283 sbthcl 7542 php 7604 inf0 7937 unctb 8484 fin1a2lem12 8690 axcc2lem 8715 axcclem 8736 brdom3 8805 brdom5 8806 brdom4 8807 pwcfsdom 8857 smobeth 8860 fpwwe2lem8 8914 fpwwe2lem9 8915 fpwwe2lem12 8918 pwxpndom2 8942 pwcdandom 8944 gchac 8958 wunex3 9018 inar1 9052 gruina 9095 ltsopi 9167 recmulnq 9243 prcdnq 9272 ltrel 9549 lerel 9551 cnexALT 11097 dfle2 11234 dflt2 11235 uzrdg0i 11898 ltwefz 11902 fzennn 11906 faclbnd4lem1 12185 hashsslei 12293 0csh0 12547 isercolllem1 13259 zsum 13312 sum0 13315 xpnnenOLD 13609 znnen 13612 qnnen 13613 rpnnen 13626 ruc 13642 nthruc 13650 nthruz 13651 phicl2 13960 pwsle 14548 xpsc0 14616 xpsc1 14617 relfull 14936 relfth 14937 gicer 15922 oppglsm 16261 efgrelexlemb 16367 isunit 16871 opsrtoslem2 17689 pjpm 18257 1stcfb 19180 2ndc1stc 19186 2ndcctbss 19190 2ndcdisj2 19192 2ndcsep 19194 hmpher 19488 met1stc 20227 re2ndc 20509 iccpnfhmeo 20648 xrhmeo 20649 xrcmp 20651 xrcon 20652 dyadmbl 21212 opnmblALT 21215 vitalilem2 21221 vitalilem3 21222 vitali 21225 mbfimaopnlem 21265 mbfsup 21274 dgrval 21828 dgrcl 21833 dgrub 21834 dgrlb 21836 aannenlem3 21928 dvrelog 22214 logcn 22224 logccv 22240 ppiub 22675 lgsquadlem1 22825 lgsquadlem2 22826 dirith2 22909 usgraexmpldifpr 23469 usgraexmpl 23470 konigsberg 23759 nvrel 24131 phrel 24366 bnrel 24419 hlrel 24442 pjnormi 25275 lnopunilem1 25565 lnophmlem1 25571 xrge0infssd 26204 ssnnssfz 26220 xrge0iifiso 26509 oms0 26853 oddpwdc 26880 erdszelem4 27225 erdszelem8 27229 supfz 27529 inffz 27530 elrn3 27716 omsinds 27823 naim1i 28376 naim2i 28377 mont 28398 onpsstopbas 28419 wl-equsal1i 28519 wl-sbcom2d 28534 mblfinlem1 28575 trer 28658 fneer 28707 incsequz2 28792 cncfres 28811 heiborlem3 28859 rencldnfilem 29306 pellexlem4 29320 pellexlem5 29321 ttac 29532 idomsubgmo 29710 areaquad 29739 lhe4.4ex1a 29750 disjxwwlks 30515 disjxwwlkn 30711 ssnn0ssfz 30888 suprfinzcl 30892 zlmodzxzldeplem 31158 eel0001 31768 eel0000 31769 eel00001 31771 eel00000 31772 e000 31817 e00 31818 bnj1023 32091 bnj1109 32097 bj-mp2c 32381 bj-mp2d 32382 bj-alrimih 32468 diclspsn 35162 dih1dimatlem 35297 |
Copyright terms: Public domain | W3C validator |