Theorem anabsi7 672

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  syldbl2  842  nelrdva  3664  elunii  4869  ordelord  6340  fvelrn  7023  onsucuni2  7778  fnfi  9106  prnmax  10910  relexpindlem  14990  opreu2reuALT  32533  ralssiun  37583  monotoddzz  43221  oddcomabszz  43222  flcidc  43448  fmul01  45862  fprodcnlem  45881  stoweidlem4  46284  stoweidlem20  46300  stoweidlem22  46302  stoweidlem27  46307  stoweidlem30  46310  stoweidlem51  46331  stoweidlem59  46339  fourierdlem21  46408  fourierdlem89  46475  fourierdlem90  46476  fourierdlem91  46477  fourierdlem104  46490