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  857  sbcof2  1834  rgen2a  2561  rspct  2874  po2nr  4364  ordsuc  4619  funssres  5322  2elresin  5396  f1imass  5856  smoel  6399  tfri3  6466  nnmass  6586  sbthlem1  7074  genpcdl  7652  genpcuu  7653  recexprlemss1l  7768  recexprlemss1u  7769  grpid  13446  uniopn  14548  elabgft1  15853  bj-rspgt  15861