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

Theorem mpdi 40
Description: A nested modus ponens deduction. (Contributed by NM, 16-Apr-2005.) (Proof shortened by O'Cat, 15-Jan-2008.)
Hypotheses
Ref Expression
mpdi.1  |-  ( ps 
->  ch )
mpdi.2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
Assertion
Ref Expression
mpdi  |-  ( ph  ->  ( ps  ->  th )
)

Proof of Theorem mpdi
StepHypRef Expression
1 mpdi.1 . . 3  |-  ( ps 
->  ch )
21a1i 11 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 mpdi.2 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
42, 3mpdd 38 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  mpii  41  pm2.43d  46  impt  151  suctrALT  4656  tfrlem9  6638  axcc2lem  8308  axdc3lem4  8325  fpwwe2lem8  8504  tskcard  8648  nqereu  8798  mulcmpblnr  8941  lbzbi  10556  ndvdsadd  12920  gcdneg  13018  ulmcaulem  20302  predpo  25451  wfrlem12  25541  frrlem11  25586  brabg2  26398  neificl  26440  frgrawopreglem4  28363
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator