Theorem nncand 11439

Description: Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
negidd.1	⊢ (𝜑 → 𝐴 ∈ ℂ)
pncand.2	⊢ (𝜑 → 𝐵 ∈ ℂ)

Assertion

Ref	Expression
nncand	⊢ (𝜑 → (𝐴 − (𝐴 − 𝐵)) = 𝐵)

Proof of Theorem nncand

Step	Hyp	Ref	Expression
1		negidd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		pncand.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℂ)
3		nncan 11352	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − (𝐴 − 𝐵)) = 𝐵)
4	1, 2, 3	syl2anc 584	1 ⊢ (𝜑 → (𝐴 − (𝐴 − 𝐵)) = 𝐵)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2105  (class class class)co 7338  ℂcc 10971   − cmin 11307

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-sep 5244  ax-nul 5251  ax-pow 5309  ax-pr 5373  ax-un 7651  ax-resscn 11030  ax-1cn 11031  ax-icn 11032  ax-addcl 11033  ax-addrcl 11034  ax-mulcl 11035  ax-mulrcl 11036  ax-mulcom 11037  ax-addass 11038  ax-mulass 11039  ax-distr 11040  ax-i2m1 11041  ax-1ne0 11042  ax-1rid 11043  ax-rnegex 11044  ax-rrecex 11045  ax-cnre 11046  ax-pre-lttri 11047  ax-pre-lttrn 11048  ax-pre-ltadd 11049

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3350  df-rab 3404  df-v 3443  df-sbc 3728  df-csb 3844  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4271  df-if 4475  df-pw 4550  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4854  df-br 5094  df-opab 5156  df-mpt 5177  df-id 5519  df-po 5533  df-so 5534  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6432  df-fun 6482  df-fn 6483  df-f 6484  df-f1 6485  df-fo 6486  df-f1o 6487  df-fv 6488  df-riota 7294  df-ov 7341  df-oprab 7342  df-mpo 7343  df-er 8570  df-en 8806  df-dom 8807  df-sdom 8808  df-pnf 11113  df-mnf 11114  df-ltxr 11116  df-sub 11309

This theorem is referenced by:  moddiffl  13704  flmod  13707  ccatswrd  14480  o1dif  15439  fprodser  15759  fprodrev  15787  fallfacval3  15822  efaddlem  15902  4sqlem5  16741  mul4sqlem  16752  4sqlem14  16757  znunit  20878  coe1tmmul2  21554  blssps  23684  blss  23685  metdstri  24121  ivthlem3  24724  ioorcl2  24843  vitalilem2  24880  dvexp3  25249  dvcvx  25291  iblulm  25673  chordthmlem4  26092  heron  26095  cubic  26106  dquartlem1  26108  birthdaylem2  26209  lgamgulmlem2  26286  lgamcvg2  26311  ftalem2  26330  basellem3  26339  gausslemma2dlem1a  26620  lgsquadlem1  26635  addsqrexnreu  26697  pntrlog2bndlem4  26835  axsegconlem1  27575  lt2addrd  31361  ballotlemsf1o  32780  revpfxsfxrev  33376  swrdrevpfx  33377  bcprod  33996  irrdiff  35653  sticksstones12a  40421  sticksstones12  40422  fltnltalem  40812  fltnlta  40813  lzenom  40905  rmspecfund  41044  fzmaxdif  41117  jm2.18  41124  jm2.19  41129  jm2.20nn  41133  supxrgere  43259  lptre2pt  43569  ioodvbdlimc2lem  43863  dvnprodlem1  43875  dvnprodlem2  43876  fourierdlem4  44040  fourierdlem26  44062  fourierdlem42  44078  fourierdlem48  44083  fourierdlem65  44100  fouriersw  44160  sge0gtfsumgt  44370  meaiininclem  44413  fmtnorec2lem  45412  goldbachthlem2  45416  pw2m1lepw2m1  46279  eenglngeehlnmlem2  46502  itsclquadb  46540