![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sub32d | Structured version Visualization version GIF version |
Description: Swap the second and third terms in a double subtraction. (Contributed by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
negidd.1 | ⊢ (𝜑 → 𝐴 ∈ ℂ) |
pncand.2 | ⊢ (𝜑 → 𝐵 ∈ ℂ) |
subaddd.3 | ⊢ (𝜑 → 𝐶 ∈ ℂ) |
Ref | Expression |
---|---|
sub32d | ⊢ (𝜑 → ((𝐴 − 𝐵) − 𝐶) = ((𝐴 − 𝐶) − 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | negidd.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℂ) | |
2 | pncand.2 | . 2 ⊢ (𝜑 → 𝐵 ∈ ℂ) | |
3 | subaddd.3 | . 2 ⊢ (𝜑 → 𝐶 ∈ ℂ) | |
4 | sub32 10503 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) − 𝐶) = ((𝐴 − 𝐶) − 𝐵)) | |
5 | 1, 2, 3, 4 | syl3anc 1477 | 1 ⊢ (𝜑 → ((𝐴 − 𝐵) − 𝐶) = ((𝐴 − 𝐶) − 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1628 ∈ wcel 2135 (class class class)co 6809 ℂcc 10122 − cmin 10454 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1867 ax-4 1882 ax-5 1984 ax-6 2050 ax-7 2086 ax-8 2137 ax-9 2144 ax-10 2164 ax-11 2179 ax-12 2192 ax-13 2387 ax-ext 2736 ax-sep 4929 ax-nul 4937 ax-pow 4988 ax-pr 5051 ax-un 7110 ax-resscn 10181 ax-1cn 10182 ax-icn 10183 ax-addcl 10184 ax-addrcl 10185 ax-mulcl 10186 ax-mulrcl 10187 ax-mulcom 10188 ax-addass 10189 ax-mulass 10190 ax-distr 10191 ax-i2m1 10192 ax-1ne0 10193 ax-1rid 10194 ax-rnegex 10195 ax-rrecex 10196 ax-cnre 10197 ax-pre-lttri 10198 ax-pre-lttrn 10199 ax-pre-ltadd 10200 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1073 df-3an 1074 df-tru 1631 df-ex 1850 df-nf 1855 df-sb 2043 df-eu 2607 df-mo 2608 df-clab 2743 df-cleq 2749 df-clel 2752 df-nfc 2887 df-ne 2929 df-nel 3032 df-ral 3051 df-rex 3052 df-reu 3053 df-rab 3055 df-v 3338 df-sbc 3573 df-csb 3671 df-dif 3714 df-un 3716 df-in 3718 df-ss 3725 df-nul 4055 df-if 4227 df-pw 4300 df-sn 4318 df-pr 4320 df-op 4324 df-uni 4585 df-br 4801 df-opab 4861 df-mpt 4878 df-id 5170 df-po 5183 df-so 5184 df-xp 5268 df-rel 5269 df-cnv 5270 df-co 5271 df-dm 5272 df-rn 5273 df-res 5274 df-ima 5275 df-iota 6008 df-fun 6047 df-fn 6048 df-f 6049 df-f1 6050 df-fo 6051 df-f1o 6052 df-fv 6053 df-riota 6770 df-ov 6812 df-oprab 6813 df-mpt2 6814 df-er 7907 df-en 8118 df-dom 8119 df-sdom 8120 df-pnf 10264 df-mnf 10265 df-ltxr 10267 df-sub 10456 |
This theorem is referenced by: hashfzo 13404 lswccatn0lsw 13559 revccat 13711 repswrevw 13729 isercolllem1 14590 iseralt 14610 prmdiv 15688 fldivp1 15799 efgredleme 18352 cphipval 23238 dvexp3 23936 dvfsumlem2 23985 isosctrlem2 24744 harmonicbnd4 24932 logfacrlim 25144 logexprlim 25145 lgsquadlem1 25300 rpvmasumlem 25371 dchrisumlem1 25373 mulog2sumlem3 25420 vmalogdivsum 25423 selberg2lem 25434 selberg2 25435 selberg4 25445 brbtwn2 25980 colinearalglem2 25982 colinearalglem4 25984 ipval2 27867 bj-bary1lem 33467 jm3.1lem1 38082 jm3.1lem2 38083 fourierdlem42 40865 fourierdlem89 40911 fourierdlem90 40912 fourierdlem91 40913 sigarperm 41551 pwdif 42007 m1modmmod 42822 |
Copyright terms: Public domain | W3C validator |