Theorem anabsan2 673

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 648	. 2 ⊢ ((𝜓 ∧ (𝜑 ∧ 𝜓)) → 𝜒)
3	2	anabss7 672	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  674  anandirs  678  fvreseq  7073  funcestrcsetclem7  18215  funcsetcestrclem7  18230  lmodvsdi  20905  lmodvsdir  20906  lmodvsass  20907  lss0cl  20968  phlpropd  21696  chpdmatlem3  22867  mbfimasn  25686  slmdvsdi  33194  slmdvsdir  33195  slmdvsass  33196  metider  33840  funcringcsetcALTV2lem7  48019  funcringcsetclem7ALTV  48042