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

Theorem mpdi 38
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 10 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 mpdi.2 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
42, 3mpdd 36 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  mpii  39  pm2.43d  44  impt  149  suctr  4475  tfrlem9  6401  axcc2lem  8062  axdc3lem4  8079  fpwwe2lem8  8259  tskcard  8403  nqereu  8553  mulcmpblnr  8696  lbzbi  10306  ndvdsadd  12607  gcdneg  12705  ulmcaulem  19771  predpo  24184  wfrlem12  24267  frrlem11  24293  brabg2  26366  neificl  26467
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator