Theorem anabsan2 672

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  anabss3  673  anandirs  677  fvreseq  6813  funcestrcsetclem7  17399  funcsetcestrclem7  17414  lmodvsdi  19660  lmodvsdir  19661  lmodvsass  19662  lss0cl  19721  phlpropd  20802  chpdmatlem3  21451  mbfimasn  24236  slmdvsdi  30847  slmdvsdir  30848  slmdvsass  30849  metider  31138  funcringcsetcALTV2lem7  44320  funcringcsetclem7ALTV  44343