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

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  loolin  102  pm2.18dc  867  sbcof2  1863  rgen2a  2604  rspct  2922  po2nr  4456  ordsuc  4712  funssres  5423  2elresin  5497  f1imass  5983  smoel  6575  tfri3  6642  nnmass  6764  sbthlem1  7280  genpcdl  7893  genpcuu  7894  recexprlemss1l  8009  recexprlemss1u  8010  grpid  13904  uniopn  15239  elabgft1  17023  bj-rspgt  17031