Theorem anabsan2 674

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  anabss3  675  anandirs  679  fvreseq  6974  funcestrcsetclem7  18052  funcsetcestrclem7  18067  lmodvsdi  20788  lmodvsdir  20789  lmodvsass  20790  lss0cl  20850  phlpropd  21562  chpdmatlem3  22725  mbfimasn  25531  slmdvsdi  33157  slmdvsdir  33158  slmdvsass  33159  metider  33861  funcringcsetcALTV2lem7  48280  funcringcsetclem7ALTV  48303