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  102  pm2.18dc  867  sbcof2  1863  rgen2a  2604  rspct  2922  po2nr  4449  ordsuc  4705  funssres  5415  2elresin  5489  f1imass  5970  smoel  6561  tfri3  6628  nnmass  6750  sbthlem1  7264  genpcdl  7876  genpcuu  7877  recexprlemss1l  7992  recexprlemss1u  7993  grpid  13821  uniopn  15025  elabgft1  16720  bj-rspgt  16728