Theorem anabsan2 671

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 646	. 2 ⊢ ((𝜓 ∧ (𝜑 ∧ 𝜓)) → 𝜒)
3	2	anabss7 670	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  anabss3  672  anandirs  676  fvreseq  6917  funcestrcsetclem7  17863  funcsetcestrclem7  17878  lmodvsdi  20146  lmodvsdir  20147  lmodvsass  20148  lss0cl  20208  phlpropd  20860  chpdmatlem3  21989  mbfimasn  24796  slmdvsdi  31468  slmdvsdir  31469  slmdvsass  31470  metider  31844  funcringcsetcALTV2lem7  45600  funcringcsetclem7ALTV  45623