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

Theorem pm2.43d 49
Description: Deduction absorbing redundant antecedent. (Contributed by NM, 18-Aug-1993.) (Proof shortened by O'Cat, 28-Nov-2008.)
Hypothesis
Ref Expression
pm2.43d.1  |-  ( ph  ->  ( ps  ->  ( ps  ->  ch ) ) )
Assertion
Ref Expression
pm2.43d  |-  ( ph  ->  ( ps  ->  ch ) )

Proof of Theorem pm2.43d
StepHypRef Expression
1 id 19 . 2  |-  ( ps 
->  ps )
2 pm2.43d.1 . 2  |-  ( ph  ->  ( ps  ->  ( ps  ->  ch ) ) )
31, 2mpdi 42 1  |-  ( ph  ->  ( ps  ->  ch ) )
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:  loolin  100  pm2.18dc  784  sbcof2  1732  rgen2a  2418  rspct  2695  po2nr  4066  ordsuc  4308  funssres  4966  2elresin  5035  f1imass  5439  smoel  5943  tfri3  6010  nnmass  6124  genpcdl  6760  genpcuu  6761  recexprlemss1l  6876  recexprlemss1u  6877  elabgft1  10724  bj-rspgt  10732
  Copyright terms: Public domain W3C validator