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  784  sbcof2  1732  rgen2a  2418  rspct  2695  po2nr  4066  ordsuc  4308  funssres  4966  2elresin  5035  f1imass  5439  smoel  5943  tfri3  6010  nnmass  6124  genpcdl  6760  genpcuu  6761  recexprlemss1l  6876  recexprlemss1u  6877  elabgft1  10724  bj-rspgt  10732