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  856  sbcof2  1821  rgen2a  2548  rspct  2857  po2nr  4340  ordsuc  4595  funssres  5296  2elresin  5365  f1imass  5817  smoel  6353  tfri3  6420  nnmass  6540  sbthlem1  7016  genpcdl  7579  genpcuu  7580  recexprlemss1l  7695  recexprlemss1u  7696  grpid  13111  uniopn  14169  elabgft1  15270  bj-rspgt  15278