Theorem anabsan2 664

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

Syntax hints:   → wi 4   ∧ wa 386

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 199  df-an 387

This theorem is referenced by:  anabss3  665  anandirs  669  fvreseq  6573  funcestrcsetclem7  17146  funcsetcestrclem7  17161  lmodvsdi  19249  lmodvsdir  19250  lmodvsass  19251  lss0cl  19310  phlpropd  20369  chpdmatlem3  21022  mbfimasn  23805  slmdvsdi  30309  slmdvsdir  30310  slmdvsass  30311  metider  30478  funcringcsetcALTV2lem7  42903  funcringcsetclem7ALTV  42926