MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpdd Structured version   Visualization version   Unicode version

Theorem mpdd 41
Description: A nested modus ponens deduction. Double deduction associated with ax-mp 5. Deduction associated with mpd 15. (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 29 . 2  |-  ( ph  ->  ( ( ps  ->  ch )  ->  ( ps  ->  th ) ) )
41, 3mpd 15 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  mpid  42  mpdi  43  syld  45  syl6c  66  mpteqb  5987  oprabid  6342  frxp  6933  smo11  7109  oaordex  7285  oaass  7288  omordi  7293  oeordsuc  7321  nnmordi  7358  nnmord  7359  nnaordex  7365  brecop  7482  findcard2  7837  elfiun  7970  ordiso2  8056  ordtypelem7  8065  cantnf  8224  coftr  8729  domtriomlem  8898  prlem936  9498  zindd  11065  supxrun  11630  ccatopth2  12864  cau3lem  13466  climcau  13783  divalglem8  14429  lcmf  14655  dirtr  16531  frgpnabllem1  17558  dprddisj2  17721  znrrg  19185  opnnei  20185  restntr  20247  lpcls  20429  comppfsc  20596  ufilmax  20971  ufileu  20983  flimfnfcls  21092  alexsubALTlem4  21114  qustgplem  21184  metrest  21588  caubl  22326  ulmcau  23399  ulmcn  23403  usgranloopv  25154  erclwwlksym  25591  erclwwlktr  25592  erclwwlknsym  25603  erclwwlkntr  25604  sumdmdlem  28120  bnj1280  29878  fundmpss  30456  dfon2lem8  30485  nodenselem7  30625  nodenselem8  30626  ifscgr  30860  btwnconn1lem11  30913  btwnconn2  30918  finminlem  31023  opnrebl2  31026  poimirlem21  32006  poimirlem26  32011  filbcmb  32112  seqpo  32121  mpt2bi123f  32451  mptbi12f  32455  ac6s6  32460  dia2dimlem12  34688  truniALT  36946  onfrALTlem3  36954  ee223  37056  usgr2wlkneq  39788
  Copyright terms: Public domain W3C validator