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 ) )

This proof depends on syntax axioms:   -> wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  loolin  102  pm2.18dc  867  sbcof2  1863  rgen2a  2604  rspct  2922  po2nr  4456  ordsuc  4712  funssres  5423  2elresin  5497  f1imass  5983  smoel  6576  tfri3  6643  nnmass  6765  sbthlem1  7281  genpcdl  7892  genpcuu  7893  recexprlemss1l  8008  recexprlemss1u  8009  grpid  13902  uniopn  15244  elabgft1  17028  bj-rspgt  17036