Theorem anabsan2 673

Description: Absorption of antecedent with conjunction. (Contributed by NM, 10-May-2004.)

Hypothesis

Ref	Expression
anabsan2.1	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜓)) → 𝜒)

Assertion

Ref	Expression
anabsan2	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Proof of Theorem anabsan2

Step	Hyp	Ref	Expression
1		anabsan2.1	. . 3 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜓)) → 𝜒)
2	1	an12s 648	. 2 ⊢ ((𝜓 ∧ (𝜑 ∧ 𝜓)) → 𝜒)
3	2	anabss7 672	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 397

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-an 398

This theorem is referenced by:  anabss3  674  anandirs  678  fvreseq  7042  funcestrcsetclem7  18098  funcsetcestrclem7  18113  lmodvsdi  20495  lmodvsdir  20496  lmodvsass  20497  lss0cl  20557  phlpropd  21208  chpdmatlem3  22342  mbfimasn  25149  slmdvsdi  32360  slmdvsdir  32361  slmdvsass  32362  metider  32874  funcringcsetcALTV2lem7  46940  funcringcsetclem7ALTV  46963