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  101  pm2.18dc  840  sbcof2  1782  rgen2a  2484  rspct  2777  po2nr  4226  ordsuc  4473  funssres  5160  2elresin  5229  f1imass  5668  smoel  6190  tfri3  6257  nnmass  6376  sbthlem1  6838  genpcdl  7320  genpcuu  7321  recexprlemss1l  7436  recexprlemss1u  7437  uniopn  12157  elabgft1  12974  bj-rspgt  12982
  Copyright terms: Public domain W3C validator