Theorem anabsan2 670

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 645	. 2 ⊢ ((𝜓 ∧ (𝜑 ∧ 𝜓)) → 𝜒)
3	2	anabss7 669	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 206  df-an 396

This theorem is referenced by:  anabss3  671  anandirs  675  fvreseq  6899  funcestrcsetclem7  17779  funcsetcestrclem7  17794  lmodvsdi  20061  lmodvsdir  20062  lmodvsass  20063  lss0cl  20123  phlpropd  20772  chpdmatlem3  21897  mbfimasn  24701  slmdvsdi  31370  slmdvsdir  31371  slmdvsass  31372  metider  31746  funcringcsetcALTV2lem7  45488  funcringcsetclem7ALTV  45511