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  6575  tfri3  6642  nnmass  6764  sbthlem1  7279  genpcdl  7892  genpcuu  7893  recexprlemss1l  8008  recexprlemss1u  8009  grpid  13903  uniopn  15227  elabgft1  17011  bj-rspgt  17019