Theorem anabsi7 683

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

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

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 401

This theorem is used by:  syldbl2  854  nelrdva  3667  elunii  4876  ordelord  6382  fvelrn  7071  onsucuni2  7828  fnfi  9160  prnmax  10986  relexpindlem  15107  opreu2reuALT  32834  ralssiun  38081  monotoddzz  43698  oddcomabszz  43699  flcidc  43925  fmul01  46324  fprodcnlem  46343  stoweidlem4  46746  stoweidlem20  46762  stoweidlem22  46764  stoweidlem27  46769  stoweidlem30  46772  stoweidlem51  46793  stoweidlem59  46801  fourierdlem21  46870  fourierdlem89  46937  fourierdlem90  46938  fourierdlem91  46939  fourierdlem104  46952