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  4491  tfrlem9  6417  axcc2lem  8078  axdc3lem4  8095  fpwwe2lem8  8275  tskcard  8419  nqereu  8569  mulcmpblnr  8712  lbzbi  10322  ndvdsadd  12623  gcdneg  12721  ulmcaulem  19787  predpo  24255  wfrlem12  24338  frrlem11  24364  brabg2  26469  neificl  26570
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator