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

Theorem mpdd 40
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 26 . 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  41  mpdi  42  syld  44  syl6c  64  mpteqb  5809  oprabid  6136  frxp  6703  smo11  6846  oaordex  7018  oaass  7021  omordi  7026  oeordsuc  7054  nnmordi  7091  nnmord  7092  nnaordex  7098  brecop  7214  findcard2  7573  elfiun  7701  ordiso2  7750  ordtypelem7  7759  cantnf  7922  cantnfOLD  7944  coftr  8463  domtriomlem  8632  prlem936  9237  zindd  10764  supxrun  11299  ccatopth2  12386  cau3lem  12863  climcau  13169  divalglem8  13625  dirtr  15427  frgpnabllem1  16372  dprddisj2  16559  dprddisj2OLD  16560  znrrg  18020  opnnei  18746  restntr  18808  lpcls  18990  ufilmax  19502  ufileu  19514  flimfnfcls  19623  alexsubALTlem4  19644  divstgplem  19713  metrest  20121  caubl  20840  ulmcau  21882  ulmcn  21886  usgranloopv  23319  sumdmdlem  25844  fundmpss  27599  dfon2lem8  27625  nodenselem7  27850  nodenselem8  27851  ifscgr  28097  btwnconn1lem11  28150  btwnconn2  28155  finminlem  28539  opnrebl2  28542  comppfsc  28605  filbcmb  28660  seqpo  28669  mpt2bi123f  29001  mptbi12f  29005  ac6s6  29010  erclwwlksym  30510  erclwwlktr  30511  erclwwlknsym  30526  erclwwlkntr  30527  truniALT  31344  onfrALTlem3  31348  ee223  31452  bnj1280  32107  dia2dimlem12  34816
  Copyright terms: Public domain W3C validator