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  48  impt  157  suctr  4961  tfrlem9  7051  axcc2lem  8812  axdc3lem4  8829  fpwwe2lem8  9011  tskcard  9155  nqereu  9303  lbzbi  11166  fleqceilz  11945  ndvdsadd  13921  gcdneg  14019  ulmcaulem  22523  wlkiswwlk1  24366  frgrawopreglem4  24724  predpo  28841  wfrlem12  28931  frrlem11  28976  heicant  29626  brabg2  29809  neificl  29849
  Copyright terms: Public domain W3C validator