Theorem divassd 11923

Description: An associative law for division. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
div1d.1	⊢ (𝜑 → 𝐴 ∈ ℂ)
divcld.2	⊢ (𝜑 → 𝐵 ∈ ℂ)
divmuld.3	⊢ (𝜑 → 𝐶 ∈ ℂ)
divassd.4	⊢ (𝜑 → 𝐶 ≠ 0)

Assertion

Ref	Expression
divassd	⊢ (𝜑 → ((𝐴 · 𝐵) / 𝐶) = (𝐴 · (𝐵 / 𝐶)))

Proof of Theorem divassd

Step	Hyp	Ref	Expression
1		div1d.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		divcld.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℂ)
3		divmuld.3	. 2 ⊢ (𝜑 → 𝐶 ∈ ℂ)
4		divassd.4	. 2 ⊢ (𝜑 → 𝐶 ≠ 0)
5		divass 11785	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 · 𝐵) / 𝐶) = (𝐴 · (𝐵 / 𝐶)))
6	1, 2, 3, 4, 5	syl112anc 1376	1 ⊢ (𝜑 → ((𝐴 · 𝐵) / 𝐶) = (𝐴 · (𝐵 / 𝐶)))

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109   ≠ wne 2925  (class class class)co 7340  ℂcc 10995  0cc0 10997   · cmul 11002   / cdiv 11765

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5231  ax-nul 5241  ax-pow 5300  ax-pr 5367  ax-un 7662  ax-resscn 11054  ax-1cn 11055  ax-icn 11056  ax-addcl 11057  ax-addrcl 11058  ax-mulcl 11059  ax-mulrcl 11060  ax-mulcom 11061  ax-addass 11062  ax-mulass 11063  ax-distr 11064  ax-i2m1 11065  ax-1ne0 11066  ax-1rid 11067  ax-rnegex 11068  ax-rrecex 11069  ax-cnre 11070  ax-pre-lttri 11071  ax-pre-lttrn 11072  ax-pre-ltadd 11073  ax-pre-mulgt0 11074

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rmo 3343  df-reu 3344  df-rab 3393  df-v 3435  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5089  df-opab 5151  df-mpt 5170  df-id 5508  df-po 5521  df-so 5522  df-xp 5619  df-rel 5620  df-cnv 5621  df-co 5622  df-dm 5623  df-rn 5624  df-res 5625  df-ima 5626  df-iota 6432  df-fun 6478  df-fn 6479  df-f 6480  df-f1 6481  df-fo 6482  df-f1o 6483  df-fv 6484  df-riota 7297  df-ov 7343  df-oprab 7344  df-mpo 7345  df-er 8616  df-en 8864  df-dom 8865  df-sdom 8866  df-pnf 11139  df-mnf 11140  df-xr 11141  df-ltxr 11142  df-le 11143  df-sub 11337  df-neg 11338  df-div 11766

This theorem is referenced by:  zesq  14121  discr  14135  crre  15008  abs1m  15230  sqreulem  15254  o1rlimmul  15513  geoisum1c  15774  mertenslem1  15778  eftlub  16005  lcmgcdlem  16504  cncongr2  16566  isprm5  16605  pcaddlem  16787  pockthlem  16804  mul4sqlem  16852  4sqlem17  16860  odadd1  19714  nmoleub3  25000  ipcau2  25115  pjthlem1  25318  dvrec  25840  plyeq0lem  26096  aareccl  26215  dvradcnv  26311  abelthlem7  26329  tangtx  26395  tanarg  26509  logcnlem4  26535  mcubic  26738  cubic2  26739  dquart  26744  quart1lem  26746  quart1  26747  tanatan  26810  atantan  26814  dvatan  26826  atantayl  26828  log2cnv  26835  lgamgulmlem4  26923  basellem3  26974  perfectlem2  27122  bposlem1  27176  bposlem2  27177  lgsquad2lem1  27276  chebbnd1lem2  27362  selberg3lem1  27449  selberg4lem1  27452  selberg4  27453  selberg4r  27462  pntrlog2bndlem2  27470  pntrlog2bndlem3  27471  pntrlog2bndlem4  27472  pntrlog2bndlem5  27473  pntrlog2bndlem6  27475  pntibndlem2  27483  pntlemo  27499  ostth2lem3  27527  axeuclidlem  28894  pjhthlem1  31322  quad3d  32685  constrrtlc1  33713  cos9thpinconstrlem1  33770  signsplypnf  34531  hgt750leme  34639  subfaclim  35178  circum  35664  faclimlem1  35733  faclimlem3  35735  knoppndvlem2  36504  knoppndvlem7  36509  knoppndvlem17  36519  itg2addnclem  37668  dvasin  37701  areacirclem1  37705  lcmineqlem11  42029  lcmineqlem18  42036  dvrelogpow2b  42058  aks4d1p1p7  42064  pellexlem6  42824  reglogexp  42884  sqrtcval  43631  binomcxplemwb  44338  binomcxplemnotnn0  44346  0ellimcdiv  45644  stoweidlem1  45996  wallispilem4  46063  stirlinglem3  46071  stirlinglem4  46072  stirlinglem7  46075  dirkertrigeq  46096  dirkercncflem2  46099  fourierdlem30  46132  fourierdlem83  46184  elaa2lem  46228  etransclem23  46252  etransclem24  46253  etransclem44  46273  etransclem45  46274  perfectALTVlem2  47720  itscnhlc0xyqsol  48764  itsclc0xyqsolr  48768  itsclquadb  48775