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  6384  fvelrn  7076  onsucuni2  7845  fnfi  9193  prnmax  11080  relexpindlem  15216  opreu2reuALT  33073  ralssiun  38331  monotoddzz  43950  oddcomabszz  43951  flcidc  44172  fmul01  46592  fprodcnlem  46611  stoweidlem4  47014  stoweidlem20  47030  stoweidlem22  47032  stoweidlem27  47037  stoweidlem30  47040  stoweidlem51  47061  stoweidlem59  47069  fourierdlem21  47138  fourierdlem89  47205  fourierdlem90  47206  fourierdlem91  47207  fourierdlem104  47220