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  3665  elunii  4863  ordelord  6329  fvelrn  7010  onsucuni2  7767  fnfi  9092  prnmax  10889  relexpindlem  14970  opreu2reuALT  32425  ralssiun  37401  monotoddzz  42936  oddcomabszz  42937  flcidc  43163  fmul01  45581  fprodcnlem  45600  stoweidlem4  46005  stoweidlem20  46021  stoweidlem22  46023  stoweidlem27  46028  stoweidlem30  46031  stoweidlem51  46052  stoweidlem59  46060  fourierdlem21  46129  fourierdlem89  46196  fourierdlem90  46197  fourierdlem91  46198  fourierdlem104  46211