Theorem anabsan2 863

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

Syntax hints:   → wi 4   ∧ wa 384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by:  anabss3  864  anandirs  874  fvreseq  6319  funcestrcsetclem7  16786  funcsetcestrclem7  16801  lmodvsdi  18886  lmodvsdir  18887  lmodvsass  18888  lss0cl  18947  phlpropd  20000  chpdmatlem3  20645  mbfimasn  23401  slmdvsdi  29768  slmdvsdir  29769  slmdvsass  29770  metider  29937  funcringcsetcALTV2lem7  42042  funcringcsetclem7ALTV  42065