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  7070  funcestrcsetclem7  18370  funcsetcestrclem7  18385  lmodvsdi  21211  lmodvsdir  21212  lmodvsass  21213  lss0cl  21273  phlpropd  22016  chpdmatlem3  23213  mbfimasn  26008  slmdvsdi  33875  slmdvsdir  33876  slmdvsass  33877  metider  34637  funcringcsetcALTV2lem7  49666  funcringcsetclem7ALTV  49689