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  862  sbcof2  1858  rgen2a  2586  rspct  2903  po2nr  4406  ordsuc  4661  funssres  5369  2elresin  5443  f1imass  5915  smoel  6466  tfri3  6533  nnmass  6655  sbthlem1  7156  genpcdl  7739  genpcuu  7740  recexprlemss1l  7855  recexprlemss1u  7856  grpid  13624  uniopn  14728  elabgft1  16395  bj-rspgt  16403