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

Theorem pm2.43d 50
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 43 1  |-  ( ph  ->  ( ps  ->  ch ) )
Colors of variables: wff set 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:  loolin  102  pm2.18dc  856  sbcof2  1821  rgen2a  2544  rspct  2849  po2nr  4324  ordsuc  4577  funssres  5274  2elresin  5343  f1imass  5792  smoel  6320  tfri3  6387  nnmass  6507  sbthlem1  6981  genpcdl  7543  genpcuu  7544  recexprlemss1l  7659  recexprlemss1u  7660  grpid  12976  uniopn  13938  elabgft1  14968  bj-rspgt  14976
  Copyright terms: Public domain W3C validator