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  855  sbcof2  1810  rgen2a  2531  rspct  2834  po2nr  4309  ordsuc  4562  funssres  5258  2elresin  5327  f1imass  5774  smoel  6300  tfri3  6367  nnmass  6487  sbthlem1  6955  genpcdl  7517  genpcuu  7518  recexprlemss1l  7633  recexprlemss1u  7634  grpid  12911  uniopn  13471  elabgft1  14500  bj-rspgt  14508