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  863  sbcof2  1858  rgen2a  2587  rspct  2904  po2nr  4412  ordsuc  4667  funssres  5376  2elresin  5450  f1imass  5925  smoel  6509  tfri3  6576  nnmass  6698  sbthlem1  7199  genpcdl  7782  genpcuu  7783  recexprlemss1l  7898  recexprlemss1u  7899  grpid  13685  uniopn  14795  elabgft1  16479  bj-rspgt  16487