Theorem div23d 11902

Description: A commutative/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
div23d	⊢ (𝜑 → ((𝐴 · 𝐵) / 𝐶) = ((𝐴 / 𝐶) · 𝐵))

Proof of Theorem div23d

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2107   ≠ wne 2942  (class class class)co 7350  ℂcc 10983  0cc0 10985   · cmul 10990   / cdiv 11746

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2709  ax-sep 5255  ax-nul 5262  ax-pow 5319  ax-pr 5383  ax-un 7663  ax-resscn 11042  ax-1cn 11043  ax-icn 11044  ax-addcl 11045  ax-addrcl 11046  ax-mulcl 11047  ax-mulrcl 11048  ax-mulcom 11049  ax-addass 11050  ax-mulass 11051  ax-distr 11052  ax-i2m1 11053  ax-1ne0 11054  ax-1rid 11055  ax-rnegex 11056  ax-rrecex 11057  ax-cnre 11058  ax-pre-lttri 11059  ax-pre-lttrn 11060  ax-pre-ltadd 11061  ax-pre-mulgt0 11062

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3064  df-rex 3073  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3739  df-csb 3855  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-nul 4282  df-if 4486  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4865  df-br 5105  df-opab 5167  df-mpt 5188  df-id 5529  df-po 5543  df-so 5544  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6444  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7306  df-ov 7353  df-oprab 7354  df-mpo 7355  df-er 8582  df-en 8818  df-dom 8819  df-sdom 8820  df-pnf 11125  df-mnf 11126  df-xr 11127  df-ltxr 11128  df-le 11129  df-sub 11321  df-neg 11322  df-div 11747

This theorem is referenced by:  bcpasc  14149  abslem2  15159  geolim  15690  bpolydiflem  15872  efaddlem  15910  eftlub  15926  bitsinv1lem  16256  pjthlem1  24723  itg2monolem3  25039  dvmulbr  25225  dvrecg  25259  dvmptdiv  25260  dvtaylp  25651  itgulm  25689  tanregt0  25817  logtayl2  25939  cxpeq  26032  heron  26110  dcubic2  26116  cubic2  26120  dquartlem1  26123  dquartlem2  26124  dquart  26125  quart1lem  26127  quart1  26128  dvatan  26207  atantayl  26209  jensenlem2  26259  lgamgulmlem2  26301  lgamgulmlem3  26302  ftalem2  26345  bclbnd  26550  bposlem9  26562  lgseisenlem4  26648  lgsquadlem1  26650  lgsquadlem2  26651  dchrvmasumlem1  26765  mulog2sumlem2  26805  2vmadivsumlem  26810  selberg3lem1  26827  selberg4lem1  26830  selberg4  26831  selberg3r  26839  pntrlog2bndlem4  26850  pntrlog2bndlem5  26851  pntibndlem2  26861  pntlemo  26877  brbtwn2  27640  colinearalg  27645  axsegconlem10  27661  axpaschlem  27675  axcontlem8  27706  pjhthlem1  30119  sinccvglem  34023  knoppndvlem14  34874  bj-bary1lem  35667  dvtan  36014  lcmineqlem10  40381  aks4d1p1p7  40417  binomcxplemnotnn0  42369  dvnprodlem2  43910  itgsinexp  43918  stirlinglem3  44039  stirlinglem4  44040  dirkertrigeqlem3  44063  fourierdlem95  44164  eenglngeehlnmlem1  46541  eenglngeehlnmlem2  46542