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  101  pm2.18dc  850  sbcof2  1803  rgen2a  2524  rspct  2827  po2nr  4294  ordsuc  4547  funssres  5240  2elresin  5309  f1imass  5753  smoel  6279  tfri3  6346  nnmass  6466  sbthlem1  6934  genpcdl  7481  genpcuu  7482  recexprlemss1l  7597  recexprlemss1u  7598  grpid  12742  uniopn  12793  elabgft1  13813  bj-rspgt  13821