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  3652  elunii  4856  ordelord  6341  fvelrn  7024  onsucuni2  7780  fnfi  9107  prnmax  10913  relexpindlem  15020  opreu2reuALT  32565  ralssiun  37743  monotoddzz  43395  oddcomabszz  43396  flcidc  43622  fmul01  46034  fprodcnlem  46053  stoweidlem4  46456  stoweidlem20  46472  stoweidlem22  46474  stoweidlem27  46479  stoweidlem30  46482  stoweidlem51  46503  stoweidlem59  46511  fourierdlem21  46580  fourierdlem89  46647  fourierdlem90  46648  fourierdlem91  46649  fourierdlem104  46662