Theorem anabsi7 678

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

Syntax hints:   → wi 4   ∧ wa 397

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 209  df-an 398

This theorem is referenced by:  syldbl2  848  nelrdva  3648  elunii  4846  ordelord  6336  fvelrn  7021  onsucuni2  7778  fnfi  9106  prnmax  10913  relexpindlem  15020  opreu2reuALT  32568  ralssiun  37784  monotoddzz  43403  oddcomabszz  43404  flcidc  43630  fmul01  46039  fprodcnlem  46058  stoweidlem4  46461  stoweidlem20  46477  stoweidlem22  46479  stoweidlem27  46484  stoweidlem30  46487  stoweidlem51  46508  stoweidlem59  46516  fourierdlem21  46585  fourierdlem89  46652  fourierdlem90  46653  fourierdlem91  46654  fourierdlem104  46667