Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpdd Structured version   Visualization version   GIF version

Theorem mpdd 42
 Description: A nested modus ponens deduction. Double deduction associated with ax-mp 5. Deduction associated with mpd 15. (Contributed by NM, 12-Dec-2004.)
Hypotheses
Ref Expression
mpdd.1 (𝜑 → (𝜓𝜒))
mpdd.2 (𝜑 → (𝜓 → (𝜒𝜃)))
Assertion
Ref Expression
mpdd (𝜑 → (𝜓𝜃))

Proof of Theorem mpdd
StepHypRef Expression
1 mpdd.1 . 2 (𝜑 → (𝜓𝜒))
2 mpdd.2 . . 3 (𝜑 → (𝜓 → (𝜒𝜃)))
32a2d 29 . 2 (𝜑 → ((𝜓𝜒) → (𝜓𝜃)))
41, 3mpd 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  43  mpdi  44  syld  46  syl6c  68  mpteqb  6207  oprabid  6576  frxp  7174  smo11  7348  oaordex  7525  oaass  7528  omordi  7533  oeordsuc  7561  nnmordi  7598  nnmord  7599  nnaordex  7605  brecop  7727  findcard2  8085  elfiun  8219  ordiso2  8303  ordtypelem7  8312  cantnf  8473  coftr  8978  domtriomlem  9147  prlem936  9748  zindd  11354  supxrun  12018  ccatopth2  13323  cau3lem  13942  climcau  14249  dvdsabseq  14873  divalglem8  14961  lcmf  15184  dirtr  17059  frgpnabllem1  18099  dprddisj2  18261  znrrg  19733  opnnei  20734  restntr  20796  lpcls  20978  comppfsc  21145  ufilmax  21521  ufileu  21533  flimfnfcls  21642  alexsubALTlem4  21664  qustgplem  21734  metrest  22139  caubl  22914  ulmcau  23953  ulmcn  23957  usgranloopv  25907  erclwwlksym  26342  erclwwlktr  26343  erclwwlknsym  26354  erclwwlkntr  26355  sumdmdlem  28661  bnj1280  30342  fundmpss  30910  dfon2lem8  30939  nodenselem7  31086  nodenselem8  31087  ifscgr  31321  btwnconn1lem11  31374  btwnconn2  31379  finminlem  31482  opnrebl2  31486  poimirlem21  32600  poimirlem26  32605  filbcmb  32705  seqpo  32713  mpt2bi123f  33141  mptbi12f  33145  ac6s6  33150  dia2dimlem12  35382  ntrk0kbimka  37357  truniALT  37772  onfrALTlem3  37780  ee223  37880  fmtnofac2lem  40018  usgr2wlkneq  40962  elwspths2on  41163  erclwwlkssym  41242  erclwwlkstr  41243  erclwwlksnsym  41254  erclwwlksntr  41255  setrec1lem4  42236
 Copyright terms: Public domain W3C validator