Theorem anabsan2 675

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  anabss3  676  anandirs  680  fvreseq  6986  funcestrcsetclem7  18103  funcsetcestrclem7  18118  lmodvsdi  20871  lmodvsdir  20872  lmodvsass  20873  lss0cl  20933  phlpropd  21645  chpdmatlem3  22815  mbfimasn  25609  slmdvsdi  33291  slmdvsdir  33292  slmdvsass  33293  metider  34054  funcringcsetcALTV2lem7  48784  funcringcsetclem7ALTV  48807