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

Theorem mpdd 38
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 24 . 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  39  mpdi  40  syld  42  syl6c  62  mpteqb  5811  oprabid  6097  frxp  6448  smo11  6618  oaordex  6793  oaass  6796  omordi  6801  oeordsuc  6829  nnmordi  6866  nnmord  6867  nnaordex  6873  brecop  6989  findcard2  7340  elfiun  7427  ordiso2  7476  ordtypelem7  7485  cantnf  7641  coftr  8145  domtriomlem  8314  prlem936  8916  zindd  10363  supxrun  10886  ccatopth2  11769  cau3lem  12150  climcau  12456  divalglem8  12912  dirtr  14673  frgpnabllem1  15476  dprddisj2  15589  znrrg  16838  opnnei  17176  restntr  17238  lpcls  17420  ufilmax  17931  ufileu  17943  flimfnfcls  18052  alexsubALTlem4  18073  divstgplem  18142  metrest  18546  caubl  19252  ulmcau  20303  ulmcn  20307  usgranloopv  21390  sumdmdlem  23913  fundmpss  25382  dfon2lem8  25409  nodenselem7  25634  nodenselem8  25635  ifscgr  25970  btwnconn1lem11  26023  btwnconn2  26028  finminlem  26312  opnrebl2  26315  comppfsc  26378  filbcmb  26433  seqpo  26442  truniALT  28563  onfrALTlem3  28567  onfrALTlem2  28569  ee223  28672  bnj1280  29326  dia2dimlem12  31810
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator