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  2900  po2nr  4399  ordsuc  4654  funssres  5359  2elresin  5433  f1imass  5897  smoel  6444  tfri3  6511  nnmass  6631  sbthlem1  7120  genpcdl  7702  genpcuu  7703  recexprlemss1l  7818  recexprlemss1u  7819  grpid  13567  uniopn  14669  elabgft1  16100  bj-rspgt  16108