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  5785  oprabid  6114  frxp  6681  smo11  6821  oaordex  6993  oaass  6996  omordi  7001  oeordsuc  7029  nnmordi  7066  nnmord  7067  nnaordex  7073  brecop  7189  findcard2  7548  elfiun  7676  ordiso2  7725  ordtypelem7  7734  cantnf  7897  cantnfOLD  7919  coftr  8438  domtriomlem  8607  prlem936  9212  zindd  10739  supxrun  11274  ccatopth2  12361  cau3lem  12838  climcau  13144  divalglem8  13600  dirtr  15402  frgpnabllem1  16344  dprddisj2  16527  dprddisj2OLD  16528  znrrg  17957  opnnei  18683  restntr  18745  lpcls  18927  ufilmax  19439  ufileu  19451  flimfnfcls  19560  alexsubALTlem4  19581  divstgplem  19650  metrest  20058  caubl  20777  ulmcau  21819  ulmcn  21823  usgranloopv  23232  sumdmdlem  25757  fundmpss  27506  dfon2lem8  27532  nodenselem7  27757  nodenselem8  27758  ifscgr  28004  btwnconn1lem11  28057  btwnconn2  28062  finminlem  28438  opnrebl2  28441  comppfsc  28504  filbcmb  28559  seqpo  28568  mpt2bi123f  28900  mptbi12f  28904  ac6s6  28909  erclwwlksym  30409  erclwwlktr  30410  erclwwlknsym  30425  erclwwlkntr  30426  truniALT  31081  onfrALTlem3  31085  onfrALTlem2  31087  ee223  31190  bnj1280  31845  dia2dimlem12  34442
  Copyright terms: Public domain W3C validator