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  6994  funcestrcsetclem7  18083  funcsetcestrclem7  18098  lmodvsdi  20767  lmodvsdir  20768  lmodvsass  20769  lss0cl  20829  phlpropd  21540  chpdmatlem3  22703  mbfimasn  25509  slmdvsdi  33141  slmdvsdir  33142  slmdvsass  33143  metider  33857  funcringcsetcALTV2lem7  48257  funcringcsetclem7ALTV  48280