Theorem anabsan2 674

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 649	. 2 ⊢ ((𝜓 ∧ (𝜑 ∧ 𝜓)) → 𝜒)
3	2	anabss7 673	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  675  anandirs  679  fvreseq  7012  funcestrcsetclem7  18107  funcsetcestrclem7  18122  lmodvsdi  20791  lmodvsdir  20792  lmodvsass  20793  lss0cl  20853  phlpropd  21564  chpdmatlem3  22727  mbfimasn  25533  slmdvsdi  33168  slmdvsdir  33169  slmdvsass  33170  metider  33884  funcringcsetcALTV2lem7  48284  funcringcsetclem7ALTV  48307