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  3673  elunii  4872  ordelord  6342  fvelrn  7030  onsucuni2  7789  fnfi  9119  prnmax  10924  relexpindlem  15005  opreu2reuALT  32456  ralssiun  37388  monotoddzz  42925  oddcomabszz  42926  flcidc  43152  fmul01  45571  fprodcnlem  45590  stoweidlem4  45995  stoweidlem20  46011  stoweidlem22  46013  stoweidlem27  46018  stoweidlem30  46021  stoweidlem51  46042  stoweidlem59  46050  fourierdlem21  46119  fourierdlem89  46186  fourierdlem90  46187  fourierdlem91  46188  fourierdlem104  46201