Theorem anabsan2 880

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 860	. 2 ⊢ ((𝜓 ∧ (𝜑 ∧ 𝜓)) → 𝜒)
3	2	anabss7 879	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  881  anandirs  891  fvreseq  6359  funcestrcsetclem7  16833  funcsetcestrclem7  16848  lmodvsdi  18934  lmodvsdir  18935  lmodvsass  18936  lss0cl  18995  phlpropd  20048  chpdmatlem3  20693  mbfimasn  23446  slmdvsdi  29896  slmdvsdir  29897  slmdvsass  29898  metider  30065  funcringcsetcALTV2lem7  42367  funcringcsetclem7ALTV  42390