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	⊢ (𝜑 → (𝜓 → (𝜓 → 𝜒)))

Assertion

Ref	Expression
pm2.43d	⊢ (𝜑 → (𝜓 → 𝜒))

Proof of Theorem pm2.43d

Step	Hyp	Ref	Expression
1		id 19	. 2 ⊢ (𝜓 → 𝜓)
2		pm2.43d.1	. 2 ⊢ (𝜑 → (𝜓 → (𝜓 → 𝜒)))
3	1, 2	mpdi 43	1 ⊢ (𝜑 → (𝜓 → 𝜒))

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  867  sbcof2  1863  rgen2a  2604  rspct  2922  po2nr  4452  ordsuc  4708  funssres  5418  2elresin  5492  f1imass  5974  smoel  6565  tfri3  6632  nnmass  6754  sbthlem1  7268  genpcdl  7880  genpcuu  7881  recexprlemss1l  7996  recexprlemss1u  7997  grpid  13827  uniopn  15085  elabgft1  16789  bj-rspgt  16797