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

Theorem mpdd 36
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 23 . 2  |-  ( ph  ->  ( ( ps  ->  ch )  ->  ( ps  ->  th ) ) )
41, 3mpd 14 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  mpid  37  mpdi  38  syld  40  syl6c  60  ax12b  1655  mpteqb  5614  oprabid  5882  frxp  6225  smo11  6381  oaordex  6556  oaass  6559  omordi  6564  oeordsuc  6592  nnmordi  6629  nnmord  6630  nnaordex  6636  brecop  6751  findcard2  7098  elfiun  7183  ordiso2  7230  ordtypelem7  7239  cantnf  7395  coftr  7899  domtriomlem  8068  prlem936  8671  zindd  10113  supxrun  10634  ccatopth2  11463  cau3lem  11838  climcau  12144  divalglem8  12599  dirtr  14358  frgpnabllem1  15161  dprddisj2  15274  znrrg  16519  opnnei  16857  restntr  16912  lpcls  17092  ufilmax  17602  ufileu  17614  flimfnfcls  17723  alexsubALTlem4  17744  divstgplem  17803  metrest  18070  caubl  18733  ulmcau  19772  ulmcn  19776  sumdmdlem  22998  fundmpss  24122  dfon2lem8  24146  nodenselem7  24341  nodenselem8  24342  ifscgr  24667  btwnconn1lem11  24720  btwnconn2  24725  limptlimpr2lem1  25574  mrdmcd  25794  finminlem  26231  opnrebl2  26236  comppfsc  26307  filbcmb  26432  seqpo  26457  usgranloop  28124  truniALT  28305  onfrALTlem3  28309  onfrALTlem2  28311  ee223  28406  bnj1280  29050  dia2dimlem12  31265
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator