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  6994  funcestrcsetclem7  18081  funcsetcestrclem7  18096  lmodvsdi  20848  lmodvsdir  20849  lmodvsass  20850  lss0cl  20910  phlpropd  21622  chpdmatlem3  22796  mbfimasn  25601  slmdvsdi  33309  slmdvsdir  33310  slmdvsass  33311  metider  34072  funcringcsetcALTV2lem7  48656  funcringcsetclem7ALTV  48679