Theorem anabsi7 669

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

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  syldbl2  839  nelrdva  3710  elunii  4921  ordelord  6400  fvelrn  7092  onsucuni2  7848  fnfi  9219  prnmax  11039  relexpindlem  15081  opreu2reuALT  32448  ralssiun  37199  monotoddzz  42713  oddcomabszz  42714  flcidc  42947  fmul01  45312  fprodcnlem  45331  stoweidlem4  45736  stoweidlem20  45752  stoweidlem22  45754  stoweidlem27  45759  stoweidlem30  45762  stoweidlem51  45783  stoweidlem59  45791  fourierdlem21  45860  fourierdlem89  45927  fourierdlem90  45928  fourierdlem91  45929  fourierdlem104  45942