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  6399  fvelrn  7097  onsucuni2  7866  fnfi  9218  prnmax  11104  relexpindlem  15242  opreu2reuALT  33142  ralssiun  38521  monotoddzz  44141  oddcomabszz  44142  flcidc  44362  fmul01  46795  fprodcnlem  46814  stoweidlem4  47217  stoweidlem20  47233  stoweidlem22  47235  stoweidlem27  47240  stoweidlem30  47243  stoweidlem51  47264  stoweidlem59  47272  fourierdlem21  47341  fourierdlem89  47408  fourierdlem90  47409  fourierdlem91  47410  fourierdlem104  47423