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  101  pm2.18dc  850  sbcof2  1803  rgen2a  2524  rspct  2827  po2nr  4292  ordsuc  4545  funssres  5238  2elresin  5307  f1imass  5751  smoel  6277  tfri3  6344  nnmass  6464  sbthlem1  6932  genpcdl  7474  genpcuu  7475  recexprlemss1l  7590  recexprlemss1u  7591  grpid  12735  uniopn  12758  elabgft1  13778  bj-rspgt  13786