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

Step	Hyp	Ref	Expression
1		id 19	. 2 |- ( ps -> ps )
2		pm2.43d.1	. 2 |- ( ph -> ( ps -> ( ps -> ch ) ) )
3	1, 2	mpdi 43	1 |- ( ph -> ( ps -> ch ) )

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  845  sbcof2  1798  rgen2a  2520  rspct  2823  po2nr  4287  ordsuc  4540  funssres  5230  2elresin  5299  f1imass  5742  smoel  6268  tfri3  6335  nnmass  6455  sbthlem1  6922  genpcdl  7460  genpcuu  7461  recexprlemss1l  7576  recexprlemss1u  7577  uniopn  12639  elabgft1  13659  bj-rspgt  13667