Theorem pm2.43d 44

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 38	1 |- ( ph -> ( ps -> ch ) )

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  95  pm2.18dc  750  sbcof2  1691  rgen2a  2375  rspct  2649  po2nr  4046  ordsuc  4287  funssres  4942  2elresin  5010  f1imass  5413  smoel  5915  tfri3  5953  nnmass  6066  genpcdl  6617  genpcuu  6618  recexprlemss1l  6733  recexprlemss1u  6734  elabgft1  9917  bj-rspgt  9925