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  7037  funcestrcsetclem7  18313  funcsetcestrclem7  18328  lmodvsdi  21153  lmodvsdir  21154  lmodvsass  21155  lss0cl  21215  phlpropd  21954  chpdmatlem3  23151  mbfimasn  25946  slmdvsdi  33769  slmdvsdir  33770  slmdvsass  33771  metider  34519  funcringcsetcALTV2lem7  49362  funcringcsetclem7ALTV  49385