Theorem pm2.43d 49

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

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7

This theorem is referenced by:  loolin  100  pm2.18dc  788  sbcof2  1738  rgen2a  2429  rspct  2715  po2nr  4136  ordsuc  4379  funssres  5056  2elresin  5125  f1imass  5553  smoel  6065  tfri3  6132  nnmass  6248  sbthlem1  6666  genpcdl  7078  genpcuu  7079  recexprlemss1l  7194  recexprlemss1u  7195  uniopn  11598  elabgft1  11678  bj-rspgt  11686