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  1656  mpteqb  5576  oprabid  5844  frxp  6187  smo11  6377  oaordex  6552  oaass  6555  omordi  6560  oeordsuc  6588  nnmordi  6625  nnmord  6626  nnaordex  6632  brecop  6747  findcard2  7094  elfiun  7179  ordiso2  7226  ordtypelem7  7235  cantnf  7391  coftr  7895  domtriomlem  8064  prlem936  8667  zindd  10109  supxrun  10630  ccatopth2  11459  cau3lem  11834  climcau  12140  divalglem8  12595  dirtr  14354  frgpnabllem1  15157  dprddisj2  15270  znrrg  16515  opnnei  16853  restntr  16908  lpcls  17088  ufilmax  17598  ufileu  17610  flimfnfcls  17719  alexsubALTlem4  17740  divstgplem  17799  metrest  18066  caubl  18729  ulmcau  19768  ulmcn  19772  sumdmdlem  22994  fundmpss  23526  dfon2lem8  23550  axdenselem7  23745  axdenselem8  23746  ifscgr  24077  btwnconn1lem11  24130  btwnconn2  24135  limptlimpr2lem1  24985  mrdmcd  25205  finminlem  25642  opnrebl2  25647  comppfsc  25718  filbcmb  25843  seqpo  25868  truniALT  27588  onfrALTlem3  27592  onfrALTlem2  27594  ee223  27686  bnj1280  28329  dia2dimlem12  30544
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator