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  7060  funcestrcsetclem7  18191  funcsetcestrclem7  18206  lmodvsdi  20883  lmodvsdir  20884  lmodvsass  20885  lss0cl  20945  phlpropd  21673  chpdmatlem3  22846  mbfimasn  25667  slmdvsdi  33221  slmdvsdir  33222  slmdvsass  33223  metider  33893  funcringcsetcALTV2lem7  48212  funcringcsetclem7ALTV  48235