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  3659  elunii  4861  ordelord  6328  fvelrn  7009  onsucuni2  7764  fnfi  9087  prnmax  10886  relexpindlem  14970  opreu2reuALT  32456  ralssiun  37451  monotoddzz  43035  oddcomabszz  43036  flcidc  43262  fmul01  45679  fprodcnlem  45698  stoweidlem4  46101  stoweidlem20  46117  stoweidlem22  46119  stoweidlem27  46124  stoweidlem30  46127  stoweidlem51  46148  stoweidlem59  46156  fourierdlem21  46225  fourierdlem89  46292  fourierdlem90  46293  fourierdlem91  46294  fourierdlem104  46307