ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mpid Unicode version

Theorem mpid 42
Description: A nested modus ponens deduction. (Contributed by NM, 14-Dec-2004.)
Hypotheses
Ref Expression
mpid.1  |-  ( ph  ->  ch )
mpid.2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
Assertion
Ref Expression
mpid  |-  ( ph  ->  ( ps  ->  th )
)

Proof of Theorem mpid
StepHypRef Expression
1 mpid.1 . . 3  |-  ( ph  ->  ch )
21a1d 22 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 mpid.2 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
42, 3mpdd 41 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7
This theorem is referenced by:  mp2d  47  pm2.43a  51  embantd  56  mpan2d  422  ceqsalt  2667  rspcimdv  2745  fvimacnv  5467  riotass2  5688  pr2ne  6959  0mnnnnn0  8861  caucvgre  10593  climcn1  10916  climcn2  10917  gcdaddm  11467  dvdsgcd  11493  coprmgcdb  11562  nprm  11597  uniopn  11950  metcnp3  12435  cncfco  12491
  Copyright terms: Public domain W3C validator