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

Theorem mpdd 39
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 25 . 2  |-  ( ph  ->  ( ( ps  ->  ch )  ->  ( ps  ->  th ) ) )
41, 3mpd 15 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  mpid  40  mpdi  41  syld  43  syl6c  63  mpteqb  5820  oprabid  6106  frxp  6457  smo11  6627  oaordex  6802  oaass  6805  omordi  6810  oeordsuc  6838  nnmordi  6875  nnmord  6876  nnaordex  6882  brecop  6998  findcard2  7349  elfiun  7436  ordiso2  7485  ordtypelem7  7494  cantnf  7650  coftr  8154  domtriomlem  8323  prlem936  8925  zindd  10372  supxrun  10895  ccatopth2  11778  cau3lem  12159  climcau  12465  divalglem8  12921  dirtr  14682  frgpnabllem1  15485  dprddisj2  15598  znrrg  16847  opnnei  17185  restntr  17247  lpcls  17429  ufilmax  17940  ufileu  17952  flimfnfcls  18061  alexsubALTlem4  18082  divstgplem  18151  metrest  18555  caubl  19261  ulmcau  20312  ulmcn  20316  usgranloopv  21399  sumdmdlem  23922  fundmpss  25391  dfon2lem8  25418  nodenselem7  25643  nodenselem8  25644  ifscgr  25979  btwnconn1lem11  26032  btwnconn2  26037  finminlem  26322  opnrebl2  26325  comppfsc  26388  filbcmb  26443  seqpo  26452  truniALT  28627  onfrALTlem3  28631  onfrALTlem2  28633  ee223  28736  bnj1280  29390  dia2dimlem12  31874
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator