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  856  sbcof2  1821  rgen2a  2548  rspct  2858  po2nr  4341  ordsuc  4596  funssres  5297  2elresin  5366  f1imass  5818  smoel  6355  tfri3  6422  nnmass  6542  sbthlem1  7018  genpcdl  7581  genpcuu  7582  recexprlemss1l  7697  recexprlemss1u  7698  grpid  13114  uniopn  14180  elabgft1  15340  bj-rspgt  15348