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  7015  funcestrcsetclem7  18114  funcsetcestrclem7  18129  lmodvsdi  20798  lmodvsdir  20799  lmodvsass  20800  lss0cl  20860  phlpropd  21571  chpdmatlem3  22734  mbfimasn  25540  slmdvsdi  33175  slmdvsdir  33176  slmdvsass  33177  metider  33891  funcringcsetcALTV2lem7  48288  funcringcsetclem7ALTV  48311