Theorem anabsan2 687

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  anabss3  688  anandirs  692  fvreseq  7032  funcestrcsetclem7  18234  funcsetcestrclem7  18249  lmodvsdi  21069  lmodvsdir  21070  lmodvsass  21071  lss0cl  21131  phlpropd  21868  chpdmatlem3  23065  mbfimasn  25860  slmdvsdi  33655  slmdvsdir  33656  slmdvsass  33657  metider  34404  funcringcsetcALTV2lem7  49211  funcringcsetclem7ALTV  49234