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  3676  elunii  4876  ordelord  6354  fvelrn  7048  onsucuni2  7809  fnfi  9142  prnmax  10948  relexpindlem  15029  opreu2reuALT  32406  ralssiun  37395  monotoddzz  42932  oddcomabszz  42933  flcidc  43159  fmul01  45578  fprodcnlem  45597  stoweidlem4  46002  stoweidlem20  46018  stoweidlem22  46020  stoweidlem27  46025  stoweidlem30  46028  stoweidlem51  46049  stoweidlem59  46057  fourierdlem21  46126  fourierdlem89  46193  fourierdlem90  46194  fourierdlem91  46195  fourierdlem104  46208