Theorem anabsi7 672

Description: Absorption of antecedent into conjunction. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 18-Nov-2013.)

Hypothesis

Ref	Expression
anabsi7.1	⊢ (𝜓 → ((𝜑 ∧ 𝜓) → 𝜒))

Assertion

Ref	Expression
anabsi7	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Proof of Theorem anabsi7

Step	Hyp	Ref	Expression
1		anabsi7.1	. . 3 ⊢ (𝜓 → ((𝜑 ∧ 𝜓) → 𝜒))
2	1	anabsi6 671	. 2 ⊢ ((𝜓 ∧ 𝜑) → 𝜒)
3	2	ancoms 458	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:  syldbl2  842  nelrdva  3665  elunii  4870  ordelord  6349  fvelrn  7032  onsucuni2  7788  fnfi  9116  prnmax  10920  relexpindlem  15000  opreu2reuALT  32569  ralssiun  37689  monotoddzz  43329  oddcomabszz  43330  flcidc  43556  fmul01  45969  fprodcnlem  45988  stoweidlem4  46391  stoweidlem20  46407  stoweidlem22  46409  stoweidlem27  46414  stoweidlem30  46417  stoweidlem51  46438  stoweidlem59  46446  fourierdlem21  46515  fourierdlem89  46582  fourierdlem90  46583  fourierdlem91  46584  fourierdlem104  46597