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  1859  rgen2a  2598  rspct  2916  po2nr  4435  ordsuc  4690  funssres  5400  2elresin  5474  f1imass  5953  smoel  6544  tfri3  6611  nnmass  6733  sbthlem1  7240  genpcdl  7850  genpcuu  7851  recexprlemss1l  7966  recexprlemss1u  7967  grpid  13794  uniopn  14992  elabgft1  16676  bj-rspgt  16684