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

Theorem mpdi 42
Description: A nested modus ponens deduction. (Contributed by NM, 16-Apr-2005.) (Proof shortened by Mel L. 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 40 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:  mpii  43  pm2.43d  49  impt  159  predpo  5387  suctr  5495  wfrlem12  7034  tfrlem9  7090  axcc2lem  8850  axdc3lem4  8867  fpwwe2lem8  9047  tskcard  9191  nqereu  9339  lbzbi  11217  fleqceilz  12021  ndvdsadd  14277  gcdneg  14375  ulmcaulem  23083  wlkiswwlk1  25119  frgrawopreglem4  25476  frrlem11  30112  relowlpssretop  31294  heicant  31434  brabg2  31501  neificl  31541  el1fzopredsuc  37686
  Copyright terms: Public domain W3C validator