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  1689  mpteqb  5697  oprabid  5969  frxp  6312  smo11  6468  oaordex  6643  oaass  6646  omordi  6651  oeordsuc  6679  nnmordi  6716  nnmord  6717  nnaordex  6723  brecop  6839  findcard2  7188  elfiun  7273  ordiso2  7320  ordtypelem7  7329  cantnf  7485  coftr  7989  domtriomlem  8158  prlem936  8761  zindd  10205  supxrun  10726  ccatopth2  11559  cau3lem  11934  climcau  12240  divalglem8  12696  dirtr  14457  frgpnabllem1  15260  dprddisj2  15373  znrrg  16625  opnnei  16963  restntr  17018  lpcls  17198  ufilmax  17704  ufileu  17716  flimfnfcls  17825  alexsubALTlem4  17846  divstgplem  17905  metrest  18172  caubl  18837  ulmcau  19878  ulmcn  19882  sumdmdlem  23112  fundmpss  24680  dfon2lem8  24704  nodenselem7  24899  nodenselem8  24900  ifscgr  25226  btwnconn1lem11  25279  btwnconn2  25284  finminlem  25555  opnrebl2  25560  comppfsc  25631  filbcmb  25756  seqpo  25781  usgranloop  27553  truniALT  28050  onfrALTlem3  28054  onfrALTlem2  28056  ee223  28157  bnj1280  28812  dia2dimlem12  31334
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator