Theorem anabsan2 686

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  anabss3  687  anandirs  691  fvreseq  7033  funcestrcsetclem7  18198  funcsetcestrclem7  18213  lmodvsdi  20980  lmodvsdir  20981  lmodvsass  20982  lss0cl  21042  phlpropd  21770  chpdmatlem3  22962  mbfimasn  25756  slmdvsdi  33472  slmdvsdir  33473  slmdvsass  33474  metider  34225  funcringcsetcALTV2lem7  48945  funcringcsetclem7ALTV  48968