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  7035  funcestrcsetclem7  18197  funcsetcestrclem7  18212  lmodvsdi  21006  lmodvsdir  21007  lmodvsass  21008  lss0cl  21068  phlpropd  21805  chpdmatlem3  22997  mbfimasn  25791  slmdvsdi  33535  slmdvsdir  33536  slmdvsass  33537  metider  34284  funcringcsetcALTV2lem7  49061  funcringcsetclem7ALTV  49084