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  3662  elunii  4871  ordelord  6373  fvelrn  7064  onsucuni2  7828  fnfi  9171  prnmax  11051  relexpindlem  15183  opreu2reuALT  33006  ralssiun  38250  monotoddzz  43888  oddcomabszz  43889  flcidc  44115  fmul01  46514  fprodcnlem  46533  stoweidlem4  46936  stoweidlem20  46952  stoweidlem22  46954  stoweidlem27  46959  stoweidlem30  46962  stoweidlem51  46983  stoweidlem59  46991  fourierdlem21  47060  fourierdlem89  47127  fourierdlem90  47128  fourierdlem91  47129  fourierdlem104  47142