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  859  sbcof2  1836  rgen2a  2564  rspct  2880  po2nr  4377  ordsuc  4632  funssres  5336  2elresin  5410  f1imass  5871  smoel  6416  tfri3  6483  nnmass  6603  sbthlem1  7092  genpcdl  7674  genpcuu  7675  recexprlemss1l  7790  recexprlemss1u  7791  grpid  13538  uniopn  14640  elabgft1  16052  bj-rspgt  16060