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 6894 oprabidw 7306 oprabid 7307 frxp 7967 smo11 8195 oaordex 8389 oaass 8392 omordi 8397 oeordsuc 8425 nnmordi 8462 nnmord 8463 nnaordex 8469 brecop 8599 findcard2OLD 9056 elfiun 9189 ordiso2 9274 ordtypelem7 9283 cantnf 9451 coftr 10029 domtriomlem 10198 prlem936 10803 zindd 12421 supxrun 13050 ccatopth2 14430 cau3lem 15066 climcau 15382 dvdsabseq 16022 divalglem8 16109 lcmf 16338 dirtr 18320 frgpnabllem1 19474 dprddisj2 19642 znrrg 20773 opnnei 22271 restntr 22333 lpcls 22515 comppfsc 22683 ufilmax 23058 ufileu 23070 flimfnfcls 23179 alexsubALTlem4 23201 qustgplem 23272 metrest 23680 caubl 24472 ulmcau 25554 ulmcn 25558 usgr2wlkneq 28124 erclwwlksym 28385 erclwwlktr 28386 erclwwlknsym 28434 erclwwlkntr 28435 sumdmdlem 30780 bnj1280 33000 fundmpss 33740 dfon2lem8 33766 nodenselem8 33894 ifscgr 34346 btwnconn1lem11 34399 btwnconn2 34404 finminlem 34507 opnrebl2 34510 fvineqsneq 35583 poimirlem21 35798 poimirlem26 35803 filbcmb 35898 seqpo 35905 mpobi123f 36320 mptbi12f 36324 ac6s6 36330 dia2dimlem12 39089 ntrk0kbimka 41649 truniALT 42161 onfrALTlem3 42164 ee223 42254 paireqne 44963 fmtnofac2lem 45020 setrec1lem4 46396 |
Copyright terms: Public domain | W3C validator |