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  7042  funcestrcsetclem7  18327  funcsetcestrclem7  18342  lmodvsdi  21167  lmodvsdir  21168  lmodvsass  21169  lss0cl  21229  phlpropd  21968  chpdmatlem3  23165  mbfimasn  25960  slmdvsdi  33824  slmdvsdir  33825  slmdvsass  33826  metider  34574  funcringcsetcALTV2lem7  49500  funcringcsetclem7ALTV  49523