Theorem anabsi7 681

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  syldbl2  852  nelrdva  3670  elunii  4872  ordelord  6370  fvelrn  7059  onsucuni2  7816  fnfi  9148  prnmax  10955  relexpindlem  15078  opreu2reuALT  32678  ralssiun  37906  monotoddzz  43525  oddcomabszz  43526  flcidc  43752  fmul01  46161  fprodcnlem  46180  stoweidlem4  46583  stoweidlem20  46599  stoweidlem22  46601  stoweidlem27  46606  stoweidlem30  46609  stoweidlem51  46630  stoweidlem59  46638  fourierdlem21  46707  fourierdlem89  46774  fourierdlem90  46775  fourierdlem91  46776  fourierdlem104  46789