![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > subsubd | Structured version Visualization version GIF version |
Description: Law for double subtraction. (Contributed by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
negidd.1 | ⊢ (𝜑 → 𝐴 ∈ ℂ) |
pncand.2 | ⊢ (𝜑 → 𝐵 ∈ ℂ) |
subaddd.3 | ⊢ (𝜑 → 𝐶 ∈ ℂ) |
Ref | Expression |
---|---|
subsubd | ⊢ (𝜑 → (𝐴 − (𝐵 − 𝐶)) = ((𝐴 − 𝐵) + 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | negidd.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℂ) | |
2 | pncand.2 | . 2 ⊢ (𝜑 → 𝐵 ∈ ℂ) | |
3 | subaddd.3 | . 2 ⊢ (𝜑 → 𝐶 ∈ ℂ) | |
4 | subsub 11485 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 − (𝐵 − 𝐶)) = ((𝐴 − 𝐵) + 𝐶)) | |
5 | 1, 2, 3, 4 | syl3anc 1372 | 1 ⊢ (𝜑 → (𝐴 − (𝐵 − 𝐶)) = ((𝐴 − 𝐵) + 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1542 ∈ wcel 2107 (class class class)co 7403 ℂcc 11103 + caddc 11108 − cmin 11439 |
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 5297 ax-nul 5304 ax-pow 5361 ax-pr 5425 ax-un 7719 ax-resscn 11162 ax-1cn 11163 ax-icn 11164 ax-addcl 11165 ax-addrcl 11166 ax-mulcl 11167 ax-mulrcl 11168 ax-mulcom 11169 ax-addass 11170 ax-mulass 11171 ax-distr 11172 ax-i2m1 11173 ax-1ne0 11174 ax-1rid 11175 ax-rnegex 11176 ax-rrecex 11177 ax-cnre 11178 ax-pre-lttri 11179 ax-pre-lttrn 11180 ax-pre-ltadd 11181 |
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-reu 3378 df-rab 3434 df-v 3477 df-sbc 3776 df-csb 3892 df-dif 3949 df-un 3951 df-in 3953 df-ss 3963 df-nul 4321 df-if 4527 df-pw 4602 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4907 df-br 5147 df-opab 5209 df-mpt 5230 df-id 5572 df-po 5586 df-so 5587 df-xp 5680 df-rel 5681 df-cnv 5682 df-co 5683 df-dm 5684 df-rn 5685 df-res 5686 df-ima 5687 df-iota 6491 df-fun 6541 df-fn 6542 df-f 6543 df-f1 6544 df-fo 6545 df-f1o 6546 df-fv 6547 df-riota 7359 df-ov 7406 df-oprab 7407 df-mpo 7408 df-er 8698 df-en 8935 df-dom 8936 df-sdom 8937 df-pnf 11245 df-mnf 11246 df-ltxr 11248 df-sub 11441 |
This theorem is referenced by: subaddmulsub 11672 uzsubsubfz 13518 bcm1k 14270 swrds2m 14887 crre 15056 imval2 15093 cvgcmp 15757 arisum2 15802 mertenslem1 15825 binomfallfaclem2 15979 fallfacval4 15982 bpolydiflem 15993 bpoly3 15997 bpoly4 15998 cos01bnd 16124 prmdiv 16713 vfermltlALT 16730 dvle 25505 dvfsumlem2 25525 efif1olem2 26033 affineequiv 26307 heron 26322 dquart 26337 quartlem1 26341 acosneg 26371 efiatan2 26401 atans2 26415 birthdaylem2 26436 lgamcvg2 26538 wilthlem2 26552 basellem5 26568 gausslemma2dlem1a 26847 pntrlog2bndlem4 27062 pntrlog2bndlem5 27063 pntrlog2bndlem6 27065 colinearalglem2 28144 axsegconlem9 28162 clwlkclwwlklem2a1 29224 clwlkclwwlklem2a4 29229 clwwlkext2edg 29288 numclwwlk1lem2foalem 29583 numclwwlk1lem2fo 29590 wrdt2ind 32094 subfacp1lem5 34112 gg-dvfsumlem2 35120 poimirlem29 36454 itg2addnclem 36476 itg2addnclem3 36478 rmspecsqrtnq 41576 sub31 43934 infleinflem2 44015 stoweidlem26 44676 fourierdlem19 44776 fourierdlem63 44819 fourierdlem107 44863 ovolval5lem1 45302 fmtnorec4 46151 itcovalt2lem2lem2 47261 |
Copyright terms: Public domain | W3C validator |