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  mpteqb  5786  oprabid  6072  frxp  6423  smo11  6593  oaordex  6768  oaass  6771  omordi  6776  oeordsuc  6804  nnmordi  6841  nnmord  6842  nnaordex  6848  brecop  6964  findcard2  7315  elfiun  7401  ordiso2  7448  ordtypelem7  7457  cantnf  7613  coftr  8117  domtriomlem  8286  prlem936  8888  zindd  10335  supxrun  10858  ccatopth2  11740  cau3lem  12121  climcau  12427  divalglem8  12883  dirtr  14644  frgpnabllem1  15447  dprddisj2  15560  znrrg  16809  opnnei  17147  restntr  17208  lpcls  17390  ufilmax  17900  ufileu  17912  flimfnfcls  18021  alexsubALTlem4  18042  divstgplem  18111  metrest  18515  caubl  19221  ulmcau  20272  ulmcn  20276  usgranloopv  21359  sumdmdlem  23882  fundmpss  25344  dfon2lem8  25368  nodenselem7  25563  nodenselem8  25564  ifscgr  25890  btwnconn1lem11  25943  btwnconn2  25948  finminlem  26219  opnrebl2  26222  comppfsc  26285  filbcmb  26340  seqpo  26349  truniALT  28345  onfrALTlem3  28349  onfrALTlem2  28351  ee223  28453  bnj1280  29107  dia2dimlem12  31570
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator