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  862  sbcof2  1857  rgen2a  2585  rspct  2902  po2nr  4408  ordsuc  4663  funssres  5371  2elresin  5445  f1imass  5920  smoel  6471  tfri3  6538  nnmass  6660  sbthlem1  7161  genpcdl  7744  genpcuu  7745  recexprlemss1l  7860  recexprlemss1u  7861  grpid  13645  uniopn  14754  elabgft1  16435  bj-rspgt  16443