MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpdd 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  ax12b  1696  mpteqb  5758  oprabid  6044  frxp  6392  smo11  6562  oaordex  6737  oaass  6740  omordi  6745  oeordsuc  6773  nnmordi  6810  nnmord  6811  nnaordex  6817  brecop  6933  findcard2  7284  elfiun  7370  ordiso2  7417  ordtypelem7  7426  cantnf  7582  coftr  8086  domtriomlem  8255  prlem936  8857  zindd  10303  supxrun  10826  ccatopth2  11704  cau3lem  12085  climcau  12391  divalglem8  12847  dirtr  14608  frgpnabllem1  15411  dprddisj2  15524  znrrg  16769  opnnei  17107  restntr  17168  lpcls  17350  ufilmax  17860  ufileu  17872  flimfnfcls  17981  alexsubALTlem4  18002  divstgplem  18071  metrest  18444  caubl  19131  ulmcau  20178  ulmcn  20182  usgranloop  21265  sumdmdlem  23769  fundmpss  25146  dfon2lem8  25170  nodenselem7  25365  nodenselem8  25366  ifscgr  25692  btwnconn1lem11  25745  btwnconn2  25750  finminlem  26012  opnrebl2  26015  comppfsc  26078  filbcmb  26133  seqpo  26142  truniALT  27969  onfrALTlem3  27973  onfrALTlem2  27975  ee223  28076  bnj1280  28727  dia2dimlem12  31190
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator