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  7039  funcestrcsetclem7  18224  funcsetcestrclem7  18239  lmodvsdi  21056  lmodvsdir  21057  lmodvsass  21058  lss0cl  21118  phlpropd  21855  chpdmatlem3  23047  mbfimasn  25842  slmdvsdi  33599  slmdvsdir  33600  slmdvsass  33601  metider  34348  funcringcsetcALTV2lem7  49118  funcringcsetclem7ALTV  49141