Theorem anabsan2 673

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

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  anabss3  674  anandirs  678  fvreseq  7037  funcestrcsetclem7  18094  funcsetcestrclem7  18109  lmodvsdi  20483  lmodvsdir  20484  lmodvsass  20485  lss0cl  20545  phlpropd  21192  chpdmatlem3  22324  mbfimasn  25131  slmdvsdi  32338  slmdvsdir  32339  slmdvsass  32340  metider  32812  funcringcsetcALTV2lem7  46842  funcringcsetclem7ALTV  46865