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  4903  tfrlem9  6947  axcc2lem  8709  axdc3lem4  8726  fpwwe2lem8  8908  tskcard  9052  nqereu  9202  mulcmpblnr  9345  lbzbi  11047  fleqceilz  11803  ndvdsadd  13723  gcdneg  13821  ulmcaulem  21985  predpo  27782  wfrlem12  27872  frrlem11  27917  heicant  28567  brabg2  28750  neificl  28790  wlkiswwlk1  30465  frgrawopreglem4  30781
  Copyright terms: Public domain W3C validator