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  5778  oprabid  6064  frxp  6415  smo11  6585  oaordex  6760  oaass  6763  omordi  6768  oeordsuc  6796  nnmordi  6833  nnmord  6834  nnaordex  6840  brecop  6956  findcard2  7307  elfiun  7393  ordiso2  7440  ordtypelem7  7449  cantnf  7605  coftr  8109  domtriomlem  8278  prlem936  8880  zindd  10327  supxrun  10850  ccatopth2  11732  cau3lem  12113  climcau  12419  divalglem8  12875  dirtr  14636  frgpnabllem1  15439  dprddisj2  15552  znrrg  16801  opnnei  17139  restntr  17200  lpcls  17382  ufilmax  17892  ufileu  17904  flimfnfcls  18013  alexsubALTlem4  18034  divstgplem  18103  metrest  18507  caubl  19213  ulmcau  20264  ulmcn  20268  usgranloopv  21351  sumdmdlem  23874  fundmpss  25336  dfon2lem8  25360  nodenselem7  25555  nodenselem8  25556  ifscgr  25882  btwnconn1lem11  25935  btwnconn2  25940  finminlem  26211  opnrebl2  26214  comppfsc  26277  filbcmb  26332  seqpo  26341  truniALT  28337  onfrALTlem3  28341  onfrALTlem2  28343  ee223  28444  bnj1280  29095  dia2dimlem12  31558
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator