![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > pnpcan2d | Structured version Visualization version GIF version |
Description: Cancellation law for mixed addition and subtraction. (Contributed by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
negidd.1 | ⊢ (𝜑 → 𝐴 ∈ ℂ) |
pncand.2 | ⊢ (𝜑 → 𝐵 ∈ ℂ) |
subaddd.3 | ⊢ (𝜑 → 𝐶 ∈ ℂ) |
Ref | Expression |
---|---|
pnpcan2d | ⊢ (𝜑 → ((𝐴 + 𝐶) − (𝐵 + 𝐶)) = (𝐴 − 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | negidd.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℂ) | |
2 | pncand.2 | . 2 ⊢ (𝜑 → 𝐵 ∈ ℂ) | |
3 | subaddd.3 | . 2 ⊢ (𝜑 → 𝐶 ∈ ℂ) | |
4 | pnpcan2 10641 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐶) − (𝐵 + 𝐶)) = (𝐴 − 𝐵)) | |
5 | 1, 2, 3, 4 | syl3anc 1496 | 1 ⊢ (𝜑 → ((𝐴 + 𝐶) − (𝐵 + 𝐶)) = (𝐴 − 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1658 ∈ wcel 2166 (class class class)co 6904 ℂcc 10249 + caddc 10254 − cmin 10584 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-8 2168 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-13 2390 ax-ext 2802 ax-sep 5004 ax-nul 5012 ax-pow 5064 ax-pr 5126 ax-un 7208 ax-resscn 10308 ax-1cn 10309 ax-icn 10310 ax-addcl 10311 ax-addrcl 10312 ax-mulcl 10313 ax-mulrcl 10314 ax-mulcom 10315 ax-addass 10316 ax-mulass 10317 ax-distr 10318 ax-i2m1 10319 ax-1ne0 10320 ax-1rid 10321 ax-rnegex 10322 ax-rrecex 10323 ax-cnre 10324 ax-pre-lttri 10325 ax-pre-lttrn 10326 ax-pre-ltadd 10327 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-3or 1114 df-3an 1115 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-mo 2604 df-eu 2639 df-clab 2811 df-cleq 2817 df-clel 2820 df-nfc 2957 df-ne 2999 df-nel 3102 df-ral 3121 df-rex 3122 df-reu 3123 df-rab 3125 df-v 3415 df-sbc 3662 df-csb 3757 df-dif 3800 df-un 3802 df-in 3804 df-ss 3811 df-nul 4144 df-if 4306 df-pw 4379 df-sn 4397 df-pr 4399 df-op 4403 df-uni 4658 df-br 4873 df-opab 4935 df-mpt 4952 df-id 5249 df-po 5262 df-so 5263 df-xp 5347 df-rel 5348 df-cnv 5349 df-co 5350 df-dm 5351 df-rn 5352 df-res 5353 df-ima 5354 df-iota 6085 df-fun 6124 df-fn 6125 df-f 6126 df-f1 6127 df-fo 6128 df-f1o 6129 df-fv 6130 df-riota 6865 df-ov 6907 df-oprab 6908 df-mpt2 6909 df-er 8008 df-en 8222 df-dom 8223 df-sdom 8224 df-pnf 10392 df-mnf 10393 df-ltxr 10395 df-sub 10586 |
This theorem is referenced by: subaddeqd 10768 modvalp1 12983 modcyc 12999 addmodlteq 13039 crre 14230 amgm2 14485 addcn2 14700 iseralt 14791 telfsumo 14907 4sqlem10 16021 pcoass 23192 ipcau2 23401 ovolshftlem1 23674 ptolemy 24647 chordthmlem2 24972 chordthmlem4 24974 heron 24977 quart1lem 24994 sinasin 25028 asinsin 25031 2efiatan 25057 atantayl2 25077 basellem3 25221 basellem8 25226 lgslem1 25434 lgseisenlem1 25512 chpdifbndlem1 25654 pntpbnd2 25688 pntlemr 25703 subfacp1lem1 31706 binomcxplemrat 39388 limcperiod 40654 fperdvper 40927 wallispilem3 41077 fourierdlem65 41181 smfmullem1 41791 pwdif 42330 |
Copyright terms: Public domain | W3C validator |