Theorem anabsi7 684

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  syldbl2  855  nelrdva  3666  elunii  4875  ordelord  6383  fvelrn  7072  onsucuni2  7833  fnfi  9175  prnmax  11007  relexpindlem  15138  opreu2reuALT  32938  ralssiun  38148  monotoddzz  43771  oddcomabszz  43772  flcidc  43998  fmul01  46397  fprodcnlem  46416  stoweidlem4  46819  stoweidlem20  46835  stoweidlem22  46837  stoweidlem27  46842  stoweidlem30  46845  stoweidlem51  46866  stoweidlem59  46874  fourierdlem21  46943  fourierdlem89  47010  fourierdlem90  47011  fourierdlem91  47012  fourierdlem104  47025