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  3662  elunii  4867  ordelord  6338  fvelrn  7021  onsucuni2  7776  fnfi  9104  prnmax  10908  relexpindlem  14988  opreu2reuALT  32531  ralssiun  37581  monotoddzz  43222  oddcomabszz  43223  flcidc  43449  fmul01  45863  fprodcnlem  45882  stoweidlem4  46285  stoweidlem20  46301  stoweidlem22  46303  stoweidlem27  46308  stoweidlem30  46311  stoweidlem51  46332  stoweidlem59  46340  fourierdlem21  46409  fourierdlem89  46476  fourierdlem90  46477  fourierdlem91  46478  fourierdlem104  46491