Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > mpdd | Structured version Visualization version GIF version |
Description: A nested modus ponens deduction. Double deduction associated with ax-mp 5. Deduction associated with mpd 15. (Contributed by NM, 12-Dec-2004.) |
Ref | Expression |
---|---|
mpdd.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
mpdd.2 | ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
Ref | Expression |
---|---|
mpdd | ⊢ (𝜑 → (𝜓 → 𝜃)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpdd.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
2 | mpdd.2 | . . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) | |
3 | 2 | a2d 29 | . 2 ⊢ (𝜑 → ((𝜓 → 𝜒) → (𝜓 → 𝜃))) |
4 | 1, 3 | mpd 15 | 1 ⊢ (𝜑 → (𝜓 → 𝜃)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 |
This theorem is referenced by: mpid 44 mpdi 45 syld 47 syl6c 70 mpteqb 6299 oprabid 6677 frxp 7287 smo11 7461 oaordex 7638 oaass 7641 omordi 7646 oeordsuc 7674 nnmordi 7711 nnmord 7712 nnaordex 7718 brecop 7840 findcard2 8200 elfiun 8336 ordiso2 8420 ordtypelem7 8429 cantnf 8590 coftr 9095 domtriomlem 9264 prlem936 9869 zindd 11478 supxrun 12146 ccatopth2 13471 cau3lem 14094 climcau 14401 dvdsabseq 15035 divalglem8 15123 lcmf 15346 dirtr 17236 frgpnabllem1 18276 dprddisj2 18438 znrrg 19914 opnnei 20924 restntr 20986 lpcls 21168 comppfsc 21335 ufilmax 21711 ufileu 21723 flimfnfcls 21832 alexsubALTlem4 21854 qustgplem 21924 metrest 22329 caubl 23106 ulmcau 24149 ulmcn 24153 usgr2wlkneq 26652 elwspths2on 26853 erclwwlkssym 26935 erclwwlkstr 26936 erclwwlksnsym 26947 erclwwlksntr 26948 sumdmdlem 29277 bnj1280 31088 fundmpss 31664 dfon2lem8 31695 nodenselem8 31841 ifscgr 32151 btwnconn1lem11 32204 btwnconn2 32209 finminlem 32312 opnrebl2 32316 poimirlem21 33430 poimirlem26 33435 filbcmb 33535 seqpo 33543 mpt2bi123f 33971 mptbi12f 33975 ac6s6 33980 dia2dimlem12 36364 ntrk0kbimka 38337 truniALT 38751 onfrALTlem3 38759 ee223 38859 fmtnofac2lem 41480 setrec1lem4 42437 |
Copyright terms: Public domain | W3C validator |