Theorem anabsi7 672

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 671	. 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  842  nelrdva  3651  elunii  4855  ordelord  6345  fvelrn  7028  onsucuni2  7785  fnfi  9112  prnmax  10918  relexpindlem  15025  opreu2reuALT  32546  ralssiun  37723  monotoddzz  43371  oddcomabszz  43372  flcidc  43598  fmul01  46010  fprodcnlem  46029  stoweidlem4  46432  stoweidlem20  46448  stoweidlem22  46450  stoweidlem27  46455  stoweidlem30  46458  stoweidlem51  46479  stoweidlem59  46487  fourierdlem21  46556  fourierdlem89  46623  fourierdlem90  46624  fourierdlem91  46625  fourierdlem104  46638