![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nncand | Structured version Visualization version GIF version |
Description: Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
negidd.1 | ⊢ (𝜑 → 𝐴 ∈ ℂ) |
pncand.2 | ⊢ (𝜑 → 𝐵 ∈ ℂ) |
Ref | Expression |
---|---|
nncand | ⊢ (𝜑 → (𝐴 − (𝐴 − 𝐵)) = 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | negidd.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℂ) | |
2 | pncand.2 | . 2 ⊢ (𝜑 → 𝐵 ∈ ℂ) | |
3 | nncan 11565 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − (𝐴 − 𝐵)) = 𝐵) | |
4 | 1, 2, 3 | syl2anc 583 | 1 ⊢ (𝜑 → (𝐴 − (𝐴 − 𝐵)) = 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1537 ∈ wcel 2108 (class class class)co 7448 ℂcc 11182 − cmin 11520 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2158 ax-12 2178 ax-ext 2711 ax-sep 5317 ax-nul 5324 ax-pow 5383 ax-pr 5447 ax-un 7770 ax-resscn 11241 ax-1cn 11242 ax-icn 11243 ax-addcl 11244 ax-addrcl 11245 ax-mulcl 11246 ax-mulrcl 11247 ax-mulcom 11248 ax-addass 11249 ax-mulass 11250 ax-distr 11251 ax-i2m1 11252 ax-1ne0 11253 ax-1rid 11254 ax-rnegex 11255 ax-rrecex 11256 ax-cnre 11257 ax-pre-lttri 11258 ax-pre-lttrn 11259 ax-pre-ltadd 11260 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3or 1088 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2543 df-eu 2572 df-clab 2718 df-cleq 2732 df-clel 2819 df-nfc 2895 df-ne 2947 df-nel 3053 df-ral 3068 df-rex 3077 df-reu 3389 df-rab 3444 df-v 3490 df-sbc 3805 df-csb 3922 df-dif 3979 df-un 3981 df-in 3983 df-ss 3993 df-nul 4353 df-if 4549 df-pw 4624 df-sn 4649 df-pr 4651 df-op 4655 df-uni 4932 df-br 5167 df-opab 5229 df-mpt 5250 df-id 5593 df-po 5607 df-so 5608 df-xp 5706 df-rel 5707 df-cnv 5708 df-co 5709 df-dm 5710 df-rn 5711 df-res 5712 df-ima 5713 df-iota 6525 df-fun 6575 df-fn 6576 df-f 6577 df-f1 6578 df-fo 6579 df-f1o 6580 df-fv 6581 df-riota 7404 df-ov 7451 df-oprab 7452 df-mpo 7453 df-er 8763 df-en 9004 df-dom 9005 df-sdom 9006 df-pnf 11326 df-mnf 11327 df-ltxr 11329 df-sub 11522 |
This theorem is referenced by: moddiffl 13933 flmod 13936 ccatswrd 14716 o1dif 15676 fprodser 15997 fprodrev 16025 fallfacval3 16060 efaddlem 16141 4sqlem5 16989 mul4sqlem 17000 4sqlem14 17005 znunit 21605 coe1tmmul2 22300 blssps 24455 blss 24456 metdstri 24892 ivthlem3 25507 ioorcl2 25626 vitalilem2 25663 dvexp3 26036 dvcvx 26079 iblulm 26468 chordthmlem4 26896 heron 26899 cubic 26910 dquartlem1 26912 birthdaylem2 27013 lgamgulmlem2 27091 lgamcvg2 27116 ftalem2 27135 basellem3 27144 gausslemma2dlem1a 27427 lgsquadlem1 27442 addsqrexnreu 27504 pntrlog2bndlem4 27642 axsegconlem1 28950 lt2addrd 32758 ballotlemsf1o 34478 revpfxsfxrev 35083 swrdrevpfx 35084 bcprod 35700 irrdiff 37292 sticksstones12a 42114 sticksstones12 42115 fltnltalem 42617 fltnlta 42618 lzenom 42726 rmspecfund 42865 fzmaxdif 42938 jm2.18 42945 jm2.19 42950 jm2.20nn 42954 supxrgere 45248 lptre2pt 45561 ioodvbdlimc2lem 45855 dvnprodlem1 45867 dvnprodlem2 45868 fourierdlem4 46032 fourierdlem26 46054 fourierdlem42 46070 fourierdlem48 46075 fourierdlem65 46092 fouriersw 46152 sge0gtfsumgt 46364 meaiininclem 46407 fmtnorec2lem 47416 goldbachthlem2 47420 pw2m1lepw2m1 48249 eenglngeehlnmlem2 48472 itsclquadb 48510 |
Copyright terms: Public domain | W3C validator |