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  860  sbcof2  1856  rgen2a  2584  rspct  2901  po2nr  4404  ordsuc  4659  funssres  5366  2elresin  5440  f1imass  5910  smoel  6461  tfri3  6528  nnmass  6650  sbthlem1  7147  genpcdl  7729  genpcuu  7730  recexprlemss1l  7845  recexprlemss1u  7846  grpid  13612  uniopn  14715  elabgft1  16310  bj-rspgt  16318