Theorem anabsan2 670

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 645	. 2 ⊢ ((𝜓 ∧ (𝜑 ∧ 𝜓)) → 𝜒)
3	2	anabss7 669	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 394

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 395

This theorem is referenced by:  anabss3  671  anandirs  675  fvreseq  7040  funcestrcsetclem7  18102  funcsetcestrclem7  18117  lmodvsdi  20639  lmodvsdir  20640  lmodvsass  20641  lss0cl  20701  phlpropd  21427  chpdmatlem3  22562  mbfimasn  25381  slmdvsdi  32630  slmdvsdir  32631  slmdvsass  32632  metider  33172  funcringcsetcALTV2lem7  47028  funcringcsetclem7ALTV  47051