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  1657  mpteqb  5616  oprabid  5884  frxp  6227  smo11  6383  oaordex  6558  oaass  6561  omordi  6566  oeordsuc  6594  nnmordi  6631  nnmord  6632  nnaordex  6638  brecop  6753  findcard2  7100  elfiun  7185  ordiso2  7232  ordtypelem7  7241  cantnf  7397  coftr  7901  domtriomlem  8070  prlem936  8673  zindd  10115  supxrun  10636  ccatopth2  11465  cau3lem  11840  climcau  12146  divalglem8  12601  dirtr  14360  frgpnabllem1  15163  dprddisj2  15276  znrrg  16521  opnnei  16859  restntr  16914  lpcls  17094  ufilmax  17604  ufileu  17616  flimfnfcls  17725  alexsubALTlem4  17746  divstgplem  17805  metrest  18072  caubl  18735  ulmcau  19774  ulmcn  19778  sumdmdlem  23000  fundmpss  24124  dfon2lem8  24148  nodenselem7  24343  nodenselem8  24344  ifscgr  24669  btwnconn1lem11  24722  btwnconn2  24727  limptlimpr2lem1  25585  mrdmcd  25805  finminlem  26242  opnrebl2  26247  comppfsc  26318  filbcmb  26443  seqpo  26468  usgranloop  28135  truniALT  28361  onfrALTlem3  28365  onfrALTlem2  28367  ee223  28468  bnj1280  29123  dia2dimlem12  31338
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator