![]() |
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 7050 oprabidw 7481 oprabid 7482 frxp 8169 smo11 8422 oaordex 8616 oaass 8619 omordi 8624 oeordsuc 8652 nnmordi 8689 nnmord 8690 nnaordex 8696 brecop 8870 elfiun 9501 ordiso2 9586 ordtypelem7 9595 cantnf 9764 coftr 10344 domtriomlem 10513 prlem936 11118 zindd 12746 supxrun 13380 ccatopth2 14767 cau3lem 15405 climcau 15721 dvdsabseq 16363 divalglem8 16450 lcmf 16682 dirtr 18674 frgpnabllem1 19917 dprddisj2 20085 znrrg 21609 opnnei 23151 restntr 23213 lpcls 23395 comppfsc 23563 ufilmax 23938 ufileu 23950 flimfnfcls 24059 alexsubALTlem4 24081 qustgplem 24152 metrest 24560 caubl 25363 ulmcau 26458 ulmcn 26462 nodenselem8 27756 usgr2wlkneq 29794 erclwwlksym 30055 erclwwlktr 30056 erclwwlknsym 30104 erclwwlkntr 30105 sumdmdlem 32452 bnj1280 34998 fundmpss 35732 dfon2lem8 35756 ifscgr 36010 btwnconn1lem11 36063 btwnconn2 36068 finminlem 36286 opnrebl2 36289 fvineqsneq 37380 poimirlem21 37603 poimirlem26 37608 filbcmb 37702 seqpo 37709 mpobi123f 38124 mptbi12f 38128 ac6s6 38134 dia2dimlem12 41034 aks6d1c1p2 42068 ntrk0kbimka 44003 truniALT 44514 onfrALTlem3 44517 ee223 44607 paireqne 47387 fmtnofac2lem 47444 setrec1lem4 48788 |
Copyright terms: Public domain | W3C validator |