Theorem anabsan2 684

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

Syntax hints:   → wi 4   ∧ wa 399

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 400

This theorem is referenced by:  anabss3  685  anandirs  689  fvreseq  7016  funcestrcsetclem7  18169  funcsetcestrclem7  18184  lmodvsdi  20940  lmodvsdir  20941  lmodvsass  20942  lss0cl  21002  phlpropd  21695  chpdmatlem3  22888  mbfimasn  25682  slmdvsdi  33356  slmdvsdir  33357  slmdvsass  33358  metider  34152  funcringcsetcALTV2lem7  48879  funcringcsetclem7ALTV  48902