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  857  sbcof2  1834  rgen2a  2561  rspct  2871  po2nr  4360  ordsuc  4615  funssres  5318  2elresin  5392  f1imass  5850  smoel  6393  tfri3  6460  nnmass  6580  sbthlem1  7066  genpcdl  7639  genpcuu  7640  recexprlemss1l  7755  recexprlemss1u  7756  grpid  13415  uniopn  14517  elabgft1  15788  bj-rspgt  15796