MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpdi 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  suctr  4605  tfrlem9  6582  axcc2lem  8249  axdc3lem4  8266  fpwwe2lem8  8445  tskcard  8589  nqereu  8739  mulcmpblnr  8882  lbzbi  10496  ndvdsadd  12855  gcdneg  12953  ulmcaulem  20177  predpo  25208  wfrlem12  25291  frrlem11  25317  brabg2  26108  neificl  26150  frgrawopreglem4  27799
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator