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  2596  rspct  2914  po2nr  4430  ordsuc  4685  funssres  5395  2elresin  5469  f1imass  5947  smoel  6531  tfri3  6598  nnmass  6720  sbthlem1  7227  genpcdl  7834  genpcuu  7835  recexprlemss1l  7950  recexprlemss1u  7951  grpid  13752  uniopn  14866  elabgft1  16550  bj-rspgt  16558