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

Theorem mpdd 40
Description: A nested modus ponens deduction. (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 26 . 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  41  mpdi  42  syld  44  syl6c  64  mpteqb  5965  oprabid  6309  frxp  6894  smo11  7036  oaordex  7208  oaass  7211  omordi  7216  oeordsuc  7244  nnmordi  7281  nnmord  7282  nnaordex  7288  brecop  7405  findcard2  7761  elfiun  7891  ordiso2  7941  ordtypelem7  7950  cantnf  8113  cantnfOLD  8135  coftr  8654  domtriomlem  8823  prlem936  9426  zindd  10963  supxrun  11508  ccatopth2  12662  cau3lem  13153  climcau  13459  divalglem8  13920  dirtr  15726  frgpnabllem1  16692  dprddisj2  16901  dprddisj2OLD  16902  znrrg  18411  opnnei  19427  restntr  19489  lpcls  19671  comppfsc  19860  ufilmax  20235  ufileu  20247  flimfnfcls  20356  alexsubALTlem4  20377  qustgplem  20446  metrest  20854  caubl  21573  ulmcau  22616  ulmcn  22620  usgranloopv  24151  erclwwlksym  24587  erclwwlktr  24588  erclwwlknsym  24599  erclwwlkntr  24600  sumdmdlem  27110  mclsax  28680  fundmpss  29049  dfon2lem8  29075  nodenselem7  29300  nodenselem8  29301  ifscgr  29547  btwnconn1lem11  29600  btwnconn2  29605  finminlem  29989  opnrebl2  29992  filbcmb  30061  seqpo  30070  mpt2bi123f  30402  mptbi12f  30406  ac6s6  30411  truniALT  32609  onfrALTlem3  32613  ee223  32717  bnj1280  33372  dia2dimlem12  36089
  Copyright terms: Public domain W3C validator