Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > pncan3oi | Structured version Visualization version GIF version |
Description: Subtraction and addition of equals. Almost but not exactly the same as pncan3i 11399 and pncan 11328, this order happens often when applying "operations to both sides" so create a theorem specifically for it. A deduction version of this is available as pncand 11434. (Contributed by David A. Wheeler, 11-Oct-2018.) |
Ref | Expression |
---|---|
pncan3oi.1 | ⊢ 𝐴 ∈ ℂ |
pncan3oi.2 | ⊢ 𝐵 ∈ ℂ |
Ref | Expression |
---|---|
pncan3oi | ⊢ ((𝐴 + 𝐵) − 𝐵) = 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pncan3oi.1 | . 2 ⊢ 𝐴 ∈ ℂ | |
2 | pncan3oi.2 | . 2 ⊢ 𝐵 ∈ ℂ | |
3 | pncan 11328 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) − 𝐵) = 𝐴) | |
4 | 1, 2, 3 | mp2an 689 | 1 ⊢ ((𝐴 + 𝐵) − 𝐵) = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1540 ∈ wcel 2105 (class class class)co 7337 ℂcc 10970 + caddc 10975 − cmin 11306 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2707 ax-sep 5243 ax-nul 5250 ax-pow 5308 ax-pr 5372 ax-un 7650 ax-resscn 11029 ax-1cn 11030 ax-icn 11031 ax-addcl 11032 ax-addrcl 11033 ax-mulcl 11034 ax-mulrcl 11035 ax-mulcom 11036 ax-addass 11037 ax-mulass 11038 ax-distr 11039 ax-i2m1 11040 ax-1ne0 11041 ax-1rid 11042 ax-rnegex 11043 ax-rrecex 11044 ax-cnre 11045 ax-pre-lttri 11046 ax-pre-lttrn 11047 ax-pre-ltadd 11048 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2886 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-reu 3350 df-rab 3404 df-v 3443 df-sbc 3728 df-csb 3844 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-nul 4270 df-if 4474 df-pw 4549 df-sn 4574 df-pr 4576 df-op 4580 df-uni 4853 df-br 5093 df-opab 5155 df-mpt 5176 df-id 5518 df-po 5532 df-so 5533 df-xp 5626 df-rel 5627 df-cnv 5628 df-co 5629 df-dm 5630 df-rn 5631 df-res 5632 df-ima 5633 df-iota 6431 df-fun 6481 df-fn 6482 df-f 6483 df-f1 6484 df-fo 6485 df-f1o 6486 df-fv 6487 df-riota 7293 df-ov 7340 df-oprab 7341 df-mpo 7342 df-er 8569 df-en 8805 df-dom 8806 df-sdom 8807 df-pnf 11112 df-mnf 11113 df-ltxr 11115 df-sub 11308 |
This theorem is referenced by: mvrraddi 11339 mvlladdi 11340 climcndslem1 15660 3dvds 16139 2503prm 16938 ovolicc2lem4 24790 eff1o 25811 basellem8 26343 bposlem6 26543 bposlem8 26545 lnfn0i 30692 lmatfvlem 32063 quad3 33927 poimirlem16 35906 poimirlem17 35907 poimirlem19 35909 poimirlem20 35910 fdc 36016 heiborlem6 36087 areaquad 41318 inductionexd 42094 stoweidlem34 43919 fouriersw 44116 mvlraddi 46833 mvrladdi 46834 |
Copyright terms: Public domain | W3C validator |