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 6806 oprabidw 7213 oprabid 7214 frxp 7858 smo11 8042 oaordex 8227 oaass 8230 omordi 8235 oeordsuc 8263 nnmordi 8300 nnmord 8301 nnaordex 8307 brecop 8433 findcard2OLD 8846 elfiun 8979 ordiso2 9064 ordtypelem7 9073 cantnf 9241 coftr 9785 domtriomlem 9954 prlem936 10559 zindd 12176 supxrun 12804 ccatopth2 14180 cau3lem 14816 climcau 15132 dvdsabseq 15770 divalglem8 15857 lcmf 16086 dirtr 17974 frgpnabllem1 19124 dprddisj2 19292 znrrg 20396 opnnei 21883 restntr 21945 lpcls 22127 comppfsc 22295 ufilmax 22670 ufileu 22682 flimfnfcls 22791 alexsubALTlem4 22813 qustgplem 22884 metrest 23289 caubl 24072 ulmcau 25154 ulmcn 25158 usgr2wlkneq 27709 erclwwlksym 27970 erclwwlktr 27971 erclwwlknsym 28019 erclwwlkntr 28020 sumdmdlem 30365 bnj1280 32583 fundmpss 33326 dfon2lem8 33352 nodenselem8 33549 ifscgr 34001 btwnconn1lem11 34054 btwnconn2 34059 finminlem 34162 opnrebl2 34165 fvineqsneq 35238 poimirlem21 35453 poimirlem26 35458 filbcmb 35553 seqpo 35560 mpobi123f 35975 mptbi12f 35979 ac6s6 35985 dia2dimlem12 38744 ntrk0kbimka 41235 truniALT 41739 onfrALTlem3 41742 ee223 41832 paireqne 44544 fmtnofac2lem 44601 setrec1lem4 45896 |
Copyright terms: Public domain | W3C validator |