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  6992  funcestrcsetclem7  18112  funcsetcestrclem7  18127  lmodvsdi  20880  lmodvsdir  20881  lmodvsass  20882  lss0cl  20942  phlpropd  21635  chpdmatlem3  22805  mbfimasn  25599  slmdvsdi  33276  slmdvsdir  33277  slmdvsass  33278  metider  34038  funcringcsetcALTV2lem7  48772  funcringcsetclem7ALTV  48795