Theorem divcan3d 11992

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

Hypotheses

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

Assertion

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

Proof of Theorem divcan3d

Step	Hyp	Ref	Expression
1		div1d.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		divcld.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℂ)
3		divcld.3	. 2 ⊢ (𝜑 → 𝐵 ≠ 0)
4		divcan3 11895	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → ((𝐵 · 𝐴) / 𝐵) = 𝐴)
5	1, 2, 3, 4	syl3anc 1372	1 ⊢ (𝜑 → ((𝐵 · 𝐴) / 𝐵) = 𝐴)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2107   ≠ wne 2941  (class class class)co 7406  ℂcc 11105  0cc0 11107   · cmul 11112   / cdiv 11868

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 2704  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-mulcom 11171  ax-addass 11172  ax-mulass 11173  ax-distr 11174  ax-i2m1 11175  ax-1ne0 11176  ax-1rid 11177  ax-rnegex 11178  ax-rrecex 11179  ax-cnre 11180  ax-pre-lttri 11181  ax-pre-lttrn 11182  ax-pre-ltadd 11183  ax-pre-mulgt0 11184

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 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-po 5588  df-so 5589  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-riota 7362  df-ov 7409  df-oprab 7410  df-mpo 7411  df-er 8700  df-en 8937  df-dom 8938  df-sdom 8939  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11443  df-neg 11444  df-div 11869

This theorem is referenced by:  prodgt0  12058  mulge0b  12081  ltdivmul  12086  ledivmul  12087  zneo  12642  2tnp1ge0ge0  13791  quoremz  13817  quoremnn0ALT  13819  moddiffl  13844  zesq  14186  discr  14200  bcn1  14270  crre  15058  abslem2  15283  fallfacval4  15984  sinhval  16094  eirrlem  16144  sqrt2irrlem  16188  ltoddhalfle  16301  flodddiv4  16353  bitsp1e  16370  bitsp1o  16371  iserodd  16765  fldivp1  16827  4sqlem17  16891  smndex2dlinvh  18795  gexexlem  19715  abv1z  20433  gzrngunit  21004  cphipval2  24750  ovolunlem1a  25005  itg1mulc  25214  dvrec  25464  elqaalem3  25826  eff1olem  26049  logf1o2  26150  isosctrlem2  26314  heron  26333  dcubic2  26339  mcubic  26342  cubic2  26343  dquartlem1  26346  dquartlem2  26347  dquart  26348  cosasin  26399  efiatan2  26412  tanatan  26414  dvatan  26430  atantayl3  26434  jensen  26483  basellem3  26577  basellem5  26579  basellem8  26582  logfacrlim  26717  perfectlem2  26723  lgsquadlem1  26873  lgsquadlem2  26874  2lgslem1c  26886  2lgslem3a  26889  dchrvmasumlem1  26988  mudivsum  27023  vmalogdivsum2  27031  logsqvma  27035  selberglem2  27039  selberglem3  27040  selberg  27041  selbergr  27061  selberg3r  27062  selberg4r  27063  selberg34r  27064  pntsval2  27069  pntpbnd1a  27078  pntibndlem2  27084  axsegconlem9  28173  cdj1i  31674  subfacval2  34167  circum  34648  knoppndvlem2  35378  knoppndvlem9  35385  areacirclem1  36565  areacirclem4  36568  lcmineqlem11  40893  aks4d1p1p4  40925  sqrtcval  42378  hashnzfzclim  43067  dmmcand  44010  sumnnodd  44333  sinmulcos  44568  itgsinexp  44658  itgcoscmulx  44672  itgsincmulx  44677  stirlinglem7  44783  dirkertrigeqlem3  44803  dirkeritg  44805  dirkercncflem2  44807  fourierdlem79  44888  fourierdlem83  44892  fourierdlem95  44904  fouriercnp  44929  fourierswlem  44933  etransclem24  44961  etransclem41  44978  sfprmdvdsmersenne  46258  dfodd6  46292  dfeven4  46293  perfectALTVlem2  46377  line2  47392  itscnhlc0xyqsol  47405  itsclquadb  47416  sinhpcosh  47739