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  840  sbcof2  1782  rgen2a  2486  rspct  2782  po2nr  4231  ordsuc  4478  funssres  5165  2elresin  5234  f1imass  5675  smoel  6197  tfri3  6264  nnmass  6383  sbthlem1  6845  genpcdl  7327  genpcuu  7328  recexprlemss1l  7443  recexprlemss1u  7444  uniopn  12168  elabgft1  12985  bj-rspgt  12993