Theorem anabsi7 671

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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  syldbl2  841  nelrdva  3618  elunii  4824  ordelord  6235  fvelrn  6897  onsucuni2  7613  fnfi  8858  prnmax  10609  relexpindlem  14626  opreu2reuALT  30544  ralssiun  35315  monotoddzz  40468  oddcomabszz  40469  flcidc  40702  fmul01  42796  fprodcnlem  42815  stoweidlem4  43220  stoweidlem20  43236  stoweidlem22  43238  stoweidlem27  43243  stoweidlem30  43246  stoweidlem51  43267  stoweidlem59  43275  fourierdlem21  43344  fourierdlem89  43411  fourierdlem90  43412  fourierdlem91  43413  fourierdlem104  43426