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  3693  elunii  4893  ordelord  6379  fvelrn  7071  onsucuni2  7833  fnfi  9197  prnmax  11014  relexpindlem  15087  opreu2reuALT  32463  ralssiun  37430  monotoddzz  42934  oddcomabszz  42935  flcidc  43161  fmul01  45576  fprodcnlem  45595  stoweidlem4  46000  stoweidlem20  46016  stoweidlem22  46018  stoweidlem27  46023  stoweidlem30  46026  stoweidlem51  46047  stoweidlem59  46055  fourierdlem21  46124  fourierdlem89  46191  fourierdlem90  46192  fourierdlem91  46193  fourierdlem104  46206