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

Theorem mpdd 41
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  |-  ( ph  ->  ( ps  ->  ch ) )
mpdd.2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
Assertion
Ref Expression
mpdd  |-  ( ph  ->  ( ps  ->  th )
)

Proof of Theorem mpdd
StepHypRef Expression
1 mpdd.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
2 mpdd.2 . . 3  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32a2d 29 . 2  |-  ( ph  ->  ( ( ps  ->  ch )  ->  ( ps  ->  th ) ) )
41, 3mpd 15 1  |-  ( ph  ->  ( ps  ->  th )
)
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  42  mpdi  43  syld  45  syl6c  66  mpteqb  5980  oprabid  6332  frxp  6917  smo11  7091  oaordex  7267  oaass  7270  omordi  7275  oeordsuc  7303  nnmordi  7340  nnmord  7341  nnaordex  7347  brecop  7464  findcard2  7817  elfiun  7950  ordiso2  8030  ordtypelem7  8039  cantnf  8197  coftr  8701  domtriomlem  8870  prlem936  9471  zindd  11036  supxrun  11601  ccatopth2  12812  cau3lem  13396  climcau  13712  divalglem8  14356  lcmf  14577  dirtr  16433  frgpnabllem1  17444  dprddisj2  17607  znrrg  19067  opnnei  20067  restntr  20129  lpcls  20311  comppfsc  20478  ufilmax  20853  ufileu  20865  flimfnfcls  20974  alexsubALTlem4  20996  qustgplem  21066  metrest  21470  caubl  22170  ulmcau  23215  ulmcn  23219  usgranloopv  24951  erclwwlksym  25387  erclwwlktr  25388  erclwwlknsym  25399  erclwwlkntr  25400  sumdmdlem  27906  bnj1280  29617  fundmpss  30194  dfon2lem8  30223  nodenselem7  30361  nodenselem8  30362  ifscgr  30596  btwnconn1lem11  30649  btwnconn2  30654  finminlem  30759  opnrebl2  30762  poimirlem21  31668  poimirlem26  31673  filbcmb  31774  seqpo  31783  mpt2bi123f  32113  mptbi12f  32117  ac6s6  32122  dia2dimlem12  34355  truniALT  36542  onfrALTlem3  36550  ee223  36654
  Copyright terms: Public domain W3C validator