Theorem nncand 11628

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 11541	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − (𝐴 − 𝐵)) = 𝐵)
4	1, 2, 3	syl2anc 582	1 ⊢ (𝜑 → (𝐴 − (𝐴 − 𝐵)) = 𝐵)

Syntax hints:   → wi 4   = wceq 1534   ∈ wcel 2100  (class class class)co 7428  ℂcc 11158   − cmin 11496

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2102  ax-9 2110  ax-10 2133  ax-11 2150  ax-12 2170  ax-ext 2700  ax-sep 5305  ax-nul 5312  ax-pow 5371  ax-pr 5435  ax-un 7749  ax-resscn 11217  ax-1cn 11218  ax-icn 11219  ax-addcl 11220  ax-addrcl 11221  ax-mulcl 11222  ax-mulrcl 11223  ax-mulcom 11224  ax-addass 11225  ax-mulass 11226  ax-distr 11227  ax-i2m1 11228  ax-1ne0 11229  ax-1rid 11230  ax-rnegex 11231  ax-rrecex 11232  ax-cnre 11233  ax-pre-lttri 11234  ax-pre-lttrn 11235  ax-pre-ltadd 11236

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2062  df-mo 2532  df-eu 2561  df-clab 2707  df-cleq 2721  df-clel 2806  df-nfc 2881  df-ne 2934  df-nel 3040  df-ral 3055  df-rex 3064  df-reu 3374  df-rab 3429  df-v 3474  df-sbc 3788  df-csb 3904  df-dif 3961  df-un 3963  df-in 3965  df-ss 3975  df-nul 4334  df-if 4535  df-pw 4610  df-sn 4635  df-pr 4637  df-op 4641  df-uni 4917  df-br 5155  df-opab 5217  df-mpt 5238  df-id 5582  df-po 5596  df-so 5597  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-iota 6509  df-fun 6559  df-fn 6560  df-f 6561  df-f1 6562  df-fo 6563  df-f1o 6564  df-fv 6565  df-riota 7384  df-ov 7431  df-oprab 7432  df-mpo 7433  df-er 8739  df-en 8980  df-dom 8981  df-sdom 8982  df-pnf 11302  df-mnf 11303  df-ltxr 11305  df-sub 11498

This theorem is referenced by:  moddiffl  13908  flmod  13911  ccatswrd  14690  o1dif  15646  fprodser  15965  fprodrev  15993  fallfacval3  16028  efaddlem  16109  4sqlem5  16958  mul4sqlem  16969  4sqlem14  16974  znunit  21574  coe1tmmul2  22267  blssps  24422  blss  24423  metdstri  24859  ivthlem3  25474  ioorcl2  25593  vitalilem2  25630  dvexp3  26002  dvcvx  26045  iblulm  26434  chordthmlem4  26861  heron  26864  cubic  26875  dquartlem1  26877  birthdaylem2  26978  lgamgulmlem2  27056  lgamcvg2  27081  ftalem2  27100  basellem3  27109  gausslemma2dlem1a  27392  lgsquadlem1  27407  addsqrexnreu  27469  pntrlog2bndlem4  27607  axsegconlem1  28894  lt2addrd  32704  ballotlemsf1o  34424  revpfxsfxrev  35029  swrdrevpfx  35030  bcprod  35646  irrdiff  37119  sticksstones12a  41942  sticksstones12  41943  fltnltalem  42429  fltnlta  42430  lzenom  42542  rmspecfund  42681  fzmaxdif  42754  jm2.18  42761  jm2.19  42766  jm2.20nn  42770  supxrgere  45062  lptre2pt  45375  ioodvbdlimc2lem  45669  dvnprodlem1  45681  dvnprodlem2  45682  fourierdlem4  45846  fourierdlem26  45868  fourierdlem42  45884  fourierdlem48  45889  fourierdlem65  45906  fouriersw  45966  sge0gtfsumgt  46178  meaiininclem  46221  fmtnorec2lem  47228  goldbachthlem2  47232  pw2m1lepw2m1  48028  eenglngeehlnmlem2  48251  itsclquadb  48289