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  3679  elunii  4879  ordelord  6357  fvelrn  7051  onsucuni2  7812  fnfi  9148  prnmax  10955  relexpindlem  15036  opreu2reuALT  32413  ralssiun  37402  monotoddzz  42939  oddcomabszz  42940  flcidc  43166  fmul01  45585  fprodcnlem  45604  stoweidlem4  46009  stoweidlem20  46025  stoweidlem22  46027  stoweidlem27  46032  stoweidlem30  46035  stoweidlem51  46056  stoweidlem59  46064  fourierdlem21  46133  fourierdlem89  46200  fourierdlem90  46201  fourierdlem91  46202  fourierdlem104  46215