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

Step	Hyp	Ref	Expression
1		id 19	. 2 |- ( ps -> ps )
2		pm2.43d.1	. 2 |- ( ph -> ( ps -> ( ps -> ch ) ) )
3	1, 2	mpdi 42	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  100  pm2.18dc  783  sbcof2  1731  rgen2a  2417  rspct  2694  po2nr  4064  ordsuc  4306  funssres  4962  2elresin  5030  f1imass  5434  smoel  5938  tfri3  5976  nnmass  6089  genpcdl  6709  genpcuu  6710  recexprlemss1l  6825  recexprlemss1u  6826  elabgft1  10588  bj-rspgt  10596