Theorem anabsi7 671

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 670	. 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  841  nelrdva  3714  elunii  4917  ordelord  6408  fvelrn  7096  onsucuni2  7854  fnfi  9216  prnmax  11033  relexpindlem  15099  opreu2reuALT  32505  ralssiun  37390  monotoddzz  42932  oddcomabszz  42933  flcidc  43159  fmul01  45536  fprodcnlem  45555  stoweidlem4  45960  stoweidlem20  45976  stoweidlem22  45978  stoweidlem27  45983  stoweidlem30  45986  stoweidlem51  46007  stoweidlem59  46015  fourierdlem21  46084  fourierdlem89  46151  fourierdlem90  46152  fourierdlem91  46153  fourierdlem104  46166