Theorem anabsan2 898

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

Syntax hints:   → wi 4   ∧ wa 383

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 385

This theorem is referenced by:  anabss3  899  anandirs  909  fvreseq  6434  funcestrcsetclem7  16908  funcsetcestrclem7  16923  lmodvsdi  19009  lmodvsdir  19010  lmodvsass  19011  lss0cl  19070  phlpropd  20123  chpdmatlem3  20768  mbfimasn  23521  slmdvsdi  29998  slmdvsdir  29999  slmdvsass  30000  metider  30167  funcringcsetcALTV2lem7  42469  funcringcsetclem7ALTV  42492