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  855  sbcof2  1810  rgen2a  2531  rspct  2836  po2nr  4311  ordsuc  4564  funssres  5260  2elresin  5329  f1imass  5777  smoel  6303  tfri3  6370  nnmass  6490  sbthlem1  6958  genpcdl  7520  genpcuu  7521  recexprlemss1l  7636  recexprlemss1u  7637  grpid  12917  uniopn  13540  elabgft1  14569  bj-rspgt  14577