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 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 400

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 401

This theorem is referenced by:  syldbl2  854  nelrdva  3675  elunii  4879  ordelord  6383  fvelrn  7072  onsucuni2  7830  fnfi  9162  prnmax  10980  relexpindlem  15100  opreu2reuALT  32764  ralssiun  37976  monotoddzz  43597  oddcomabszz  43598  flcidc  43824  fmul01  46223  fprodcnlem  46242  stoweidlem4  46645  stoweidlem20  46661  stoweidlem22  46663  stoweidlem27  46668  stoweidlem30  46671  stoweidlem51  46692  stoweidlem59  46700  fourierdlem21  46769  fourierdlem89  46836  fourierdlem90  46837  fourierdlem91  46838  fourierdlem104  46851