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  1824  rgen2a  2551  rspct  2861  po2nr  4344  ordsuc  4599  funssres  5300  2elresin  5369  f1imass  5821  smoel  6358  tfri3  6425  nnmass  6545  sbthlem1  7023  genpcdl  7586  genpcuu  7587  recexprlemss1l  7702  recexprlemss1u  7703  grpid  13171  uniopn  14237  elabgft1  15424  bj-rspgt  15432