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  863  sbcof2  1859  rgen2a  2596  rspct  2913  po2nr  4429  ordsuc  4684  funssres  5394  2elresin  5468  f1imass  5946  smoel  6530  tfri3  6597  nnmass  6719  sbthlem1  7226  genpcdl  7830  genpcuu  7831  recexprlemss1l  7946  recexprlemss1u  7947  grpid  13741  uniopn  14853  elabgft1  16537  bj-rspgt  16545