Theorem anabsan2 680

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  anabss3  681  anandirs  685  fvreseq  6981  funcestrcsetclem7  18103  funcsetcestrclem7  18118  lmodvsdi  20875  lmodvsdir  20876  lmodvsass  20877  lss0cl  20937  phlpropd  21630  chpdmatlem3  22823  mbfimasn  25617  slmdvsdi  33296  slmdvsdir  33297  slmdvsass  33298  metider  34078  funcringcsetcALTV2lem7  48787  funcringcsetclem7ALTV  48810