Theorem anabsan2 859

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

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  anabss3  860  anandirs  870  fvreseq  6227  funcestrcsetclem7  16609  funcsetcestrclem7  16624  lmodvsdi  18709  lmodvsdir  18710  lmodvsass  18711  lss0cl  18768  phlpropd  19819  chpdmatlem3  20464  mbfimasn  23207  slmdvsdi  29099  slmdvsdir  29100  slmdvsass  29101  metider  29265  funcringcsetcALTV2lem7  41834  funcringcsetclem7ALTV  41857