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  788  sbcof2  1738  rgen2a  2429  rspct  2715  po2nr  4136  ordsuc  4379  funssres  5056  2elresin  5125  f1imass  5553  smoel  6065  tfri3  6132  nnmass  6248  sbthlem1  6666  genpcdl  7078  genpcuu  7079  recexprlemss1l  7194  recexprlemss1u  7195  uniopn  11598  elabgft1  11678  bj-rspgt  11686
  Copyright terms: Public domain W3C validator