P. 83 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 8201-8300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	mul32i 8201	Commutative/associative law that swaps the last two factors in a triple product. (Contributed by NM, 11-May-1999.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   =>    |- ( ( A x. B ) x. C ) = ( ( A x. C ) x. B )
Theorem	mul4i 8202	Rearrangement of 4 factors. (Contributed by NM, 16-Feb-1995.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   &    |- D e. CC   =>    |- ( ( A x. B ) x. ( C x. D ) ) = ( ( A x. C ) x. ( B x. D ) )
Theorem	addridd 8203	0 is an additive identity. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( A + 0 ) = A )
Theorem	addlidd 8204	0 is a left identity for addition. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( 0 + A ) = A )
Theorem	addcomd 8205	Addition commutes. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( A + B ) = ( B + A ) )
Theorem	mul12d 8206	Commutative/associative law that swaps the first two factors in a triple product. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( A x. ( B x. C ) ) = ( B x. ( A x. C ) ) )
Theorem	mul32d 8207	Commutative/associative law that swaps the last two factors in a triple product. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A x. B ) x. C ) = ( ( A x. C ) x. B ) )
Theorem	mul31d 8208	Commutative/associative law. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A x. B ) x. C ) = ( ( C x. B ) x. A ) )
Theorem	mul4d 8209	Rearrangement of 4 factors. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> D e. CC )   =>    |- ( ph -> ( ( A x. B ) x. ( C x. D ) ) = ( ( A x. C ) x. ( B x. D ) ) )
Theorem	muladd11r 8210	A simple product of sums expansion. (Contributed by AV, 30-Jul-2021.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( A + 1 ) x. ( B + 1 ) ) = ( ( ( A x. B ) + ( A + B ) ) + 1 ) )
Theorem	comraddd 8211	Commute RHS addition, in deduction form. (Contributed by David A. Wheeler, 11-Oct-2018.)
|- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> A = ( B + C ) )   =>    |- ( ph -> A = ( C + B ) )
4.3  Real and complex numbers - basic operations
4.3.1  Addition
Theorem	add12 8212	Commutative/associative law that swaps the first two terms in a triple sum. (Contributed by NM, 11-May-2004.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A + ( B + C ) ) = ( B + ( A + C ) ) )
Theorem	add32 8213	Commutative/associative law that swaps the last two terms in a triple sum. (Contributed by NM, 13-Nov-1999.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) + C ) = ( ( A + C ) + B ) )
Theorem	add32r 8214	Commutative/associative law that swaps the last two terms in a triple sum, rearranging the parentheses. (Contributed by Paul Chapman, 18-May-2007.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A + ( B + C ) ) = ( ( A + C ) + B ) )
Theorem	add4 8215	Rearrangement of 4 terms in a sum. (Contributed by NM, 13-Nov-1999.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A + B ) + ( C + D ) ) = ( ( A + C ) + ( B + D ) ) )
Theorem	add42 8216	Rearrangement of 4 terms in a sum. (Contributed by NM, 12-May-2005.)
|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A + B ) + ( C + D ) ) = ( ( A + C ) + ( D + B ) ) )
Theorem	add12i 8217	Commutative/associative law that swaps the first two terms in a triple sum. (Contributed by NM, 21-Jan-1997.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   =>    |- ( A + ( B + C ) ) = ( B + ( A + C ) )
Theorem	add32i 8218	Commutative/associative law that swaps the last two terms in a triple sum. (Contributed by NM, 21-Jan-1997.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   =>    |- ( ( A + B ) + C ) = ( ( A + C ) + B )
Theorem	add4i 8219	Rearrangement of 4 terms in a sum. (Contributed by NM, 9-May-1999.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   &    |- D e. CC   =>    |- ( ( A + B ) + ( C + D ) ) = ( ( A + C ) + ( B + D ) )
Theorem	add42i 8220	Rearrangement of 4 terms in a sum. (Contributed by NM, 22-Aug-1999.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   &    |- D e. CC   =>    |- ( ( A + B ) + ( C + D ) ) = ( ( A + C ) + ( D + B ) )
Theorem	add12d 8221	Commutative/associative law that swaps the first two terms in a triple sum. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( A + ( B + C ) ) = ( B + ( A + C ) ) )
Theorem	add32d 8222	Commutative/associative law that swaps the last two terms in a triple sum. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A + B ) + C ) = ( ( A + C ) + B ) )
Theorem	add4d 8223	Rearrangement of 4 terms in a sum. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> D e. CC )   =>    |- ( ph -> ( ( A + B ) + ( C + D ) ) = ( ( A + C ) + ( B + D ) ) )
Theorem	add42d 8224	Rearrangement of 4 terms in a sum. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> D e. CC )   =>    |- ( ph -> ( ( A + B ) + ( C + D ) ) = ( ( A + C ) + ( D + B ) ) )
4.3.2  Subtraction
Syntax	cmin 8225	Extend class notation to include subtraction.
class -
Syntax	cneg 8226	Extend class notation to include unary minus. The symbol -u is not a class by itself but part of a compound class definition. We do this rather than making it a formal function since it is so commonly used. Note: We use different symbols for unary minus ( -u) and subtraction cmin 8225 ( -) to prevent syntax ambiguity. For example, looking at the syntax definition co 5934, if we used the same symbol then " ( - A - B ) " could mean either " - A " minus " B", or it could represent the (meaningless) operation of classes " - " and " - B " connected with "operation" " A". On the other hand, " ( -u A - B ) " is unambiguous.
class -u A
Definition	df-sub 8227*	Define subtraction. Theorem subval 8246 shows its value (and describes how this definition works), Theorem subaddi 8341 relates it to addition, and Theorems subcli 8330 and resubcli 8317 prove its closure laws. (Contributed by NM, 26-Nov-1994.)
|- - = ( x e. CC , y e. CC |-> ( iota_ z e. CC ( y + z ) = x ) )
Definition	df-neg 8228	Define the negative of a number (unary minus). We use different symbols for unary minus ( -u) and subtraction ( -) to prevent syntax ambiguity. See cneg 8226 for a discussion of this. (Contributed by NM, 10-Feb-1995.)
|- -u A = ( 0 - A )
Theorem	cnegexlem1 8229	Addition cancellation of a real number from two complex numbers. Lemma for cnegex 8232. (Contributed by Eric Schmidt, 22-May-2007.)
|- ( ( A e. RR /\ B e. CC /\ C e. CC ) -> ( ( A + B ) = ( A + C ) <-> B = C ) )
Theorem	cnegexlem2 8230	Existence of a real number which produces a real number when multiplied by _i. (Hint: zero is such a number, although we don't need to prove that yet). Lemma for cnegex 8232. (Contributed by Eric Schmidt, 22-May-2007.)
|- E. y e. RR ( _i x. y ) e. RR
Theorem	cnegexlem3 8231*	Existence of real number difference. Lemma for cnegex 8232. (Contributed by Eric Schmidt, 22-May-2007.)
|- ( ( b e. RR /\ y e. RR ) -> E. c e. RR ( b + c ) = y )
Theorem	cnegex 8232*	Existence of the negative of a complex number. (Contributed by Eric Schmidt, 21-May-2007.)
|- ( A e. CC -> E. x e. CC ( A + x ) = 0 )
Theorem	cnegex2 8233*	Existence of a left inverse for addition. (Contributed by Scott Fenton, 3-Jan-2013.)
|- ( A e. CC -> E. x e. CC ( x + A ) = 0 )
Theorem	addcan 8234	Cancellation law for addition. Theorem I.1 of [Apostol] p. 18. (Contributed by NM, 22-Nov-1994.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) = ( A + C ) <-> B = C ) )
Theorem	addcan2 8235	Cancellation law for addition. (Contributed by NM, 30-Jul-2004.) (Revised by Scott Fenton, 3-Jan-2013.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + C ) = ( B + C ) <-> A = B ) )
Theorem	addcani 8236	Cancellation law for addition. Theorem I.1 of [Apostol] p. 18. (Contributed by NM, 27-Oct-1999.) (Revised by Scott Fenton, 3-Jan-2013.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   =>    |- ( ( A + B ) = ( A + C ) <-> B = C )
Theorem	addcan2i 8237	Cancellation law for addition. Theorem I.1 of [Apostol] p. 18. (Contributed by NM, 14-May-2003.) (Revised by Scott Fenton, 3-Jan-2013.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   =>    |- ( ( A + C ) = ( B + C ) <-> A = B )
Theorem	addcand 8238	Cancellation law for addition. Theorem I.1 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A + B ) = ( A + C ) <-> B = C ) )
Theorem	addcan2d 8239	Cancellation law for addition. Theorem I.1 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A + C ) = ( B + C ) <-> A = B ) )
Theorem	addcanad 8240	Cancelling a term on the left-hand side of a sum in an equality. Consequence of addcand 8238. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> ( A + B ) = ( A + C ) )   =>    |- ( ph -> B = C )
Theorem	addcan2ad 8241	Cancelling a term on the right-hand side of a sum in an equality. Consequence of addcan2d 8239. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> ( A + C ) = ( B + C ) )   =>    |- ( ph -> A = B )
Theorem	addneintrd 8242	Introducing a term on the left-hand side of a sum in a negated equality. Contrapositive of addcanad 8240. Consequence of addcand 8238. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> B =/= C )   =>    |- ( ph -> ( A + B ) =/= ( A + C ) )
Theorem	addneintr2d 8243	Introducing a term on the right-hand side of a sum in a negated equality. Contrapositive of addcan2ad 8241. Consequence of addcan2d 8239. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> A =/= B )   =>    |- ( ph -> ( A + C ) =/= ( B + C ) )
Theorem	0cnALT 8244	Alternate proof of 0cn 8046. (Contributed by NM, 19-Feb-2005.) (Revised by Mario Carneiro, 27-May-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
|- 0 e. CC
Theorem	negeu 8245*	Existential uniqueness of negatives. Theorem I.2 of [Apostol] p. 18. (Contributed by NM, 22-Nov-1994.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|- ( ( A e. CC /\ B e. CC ) -> E! x e. CC ( A + x ) = B )
Theorem	subval 8246*	Value of subtraction, which is the (unique) element x such that B + x = A. (Contributed by NM, 4-Aug-2007.) (Revised by Mario Carneiro, 2-Nov-2013.)
|- ( ( A e. CC /\ B e. CC ) -> ( A - B ) = ( iota_ x e. CC ( B + x ) = A ) )
Theorem	negeq 8247	Equality theorem for negatives. (Contributed by NM, 10-Feb-1995.)
|- ( A = B -> -u A = -u B )
Theorem	negeqi 8248	Equality inference for negatives. (Contributed by NM, 14-Feb-1995.)
|- A = B   =>    |- -u A = -u B
Theorem	negeqd 8249	Equality deduction for negatives. (Contributed by NM, 14-May-1999.)
|- ( ph -> A = B )   =>    |- ( ph -> -u A = -u B )
Theorem	nfnegd 8250	Deduction version of nfneg 8251. (Contributed by NM, 29-Feb-2008.) (Revised by Mario Carneiro, 15-Oct-2016.)
|- ( ph -> F/_ x A )   =>    |- ( ph -> F/_ x -u A )
Theorem	nfneg 8251	Bound-variable hypothesis builder for the negative of a complex number. (Contributed by NM, 12-Jun-2005.) (Revised by Mario Carneiro, 15-Oct-2016.)
|- F/_ x A   =>    |- F/_ x -u A
Theorem	csbnegg 8252	Move class substitution in and out of the negative of a number. (Contributed by NM, 1-Mar-2008.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
|- ( A e. V -> [_ A / x ]_ -u B = -u [_ A / x ]_ B )
Theorem	subcl 8253	Closure law for subtraction. (Contributed by NM, 10-May-1999.) (Revised by Mario Carneiro, 21-Dec-2013.)
|- ( ( A e. CC /\ B e. CC ) -> ( A - B ) e. CC )
Theorem	negcl 8254	Closure law for negative. (Contributed by NM, 6-Aug-2003.)
|- ( A e. CC -> -u A e. CC )
Theorem	negicn 8255	-u _i is a complex number (common case). (Contributed by David A. Wheeler, 7-Dec-2018.)
|- -u _i e. CC
Theorem	subf 8256	Subtraction is an operation on the complex numbers. (Contributed by NM, 4-Aug-2007.) (Revised by Mario Carneiro, 16-Nov-2013.)
|- - : ( CC X. CC ) --> CC
Theorem	subadd 8257	Relationship between subtraction and addition. (Contributed by NM, 20-Jan-1997.) (Revised by Mario Carneiro, 21-Dec-2013.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - B ) = C <-> ( B + C ) = A ) )
Theorem	subadd2 8258	Relationship between subtraction and addition. (Contributed by Scott Fenton, 5-Jul-2013.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - B ) = C <-> ( C + B ) = A ) )
Theorem	subsub23 8259	Swap subtrahend and result of subtraction. (Contributed by NM, 14-Dec-2007.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - B ) = C <-> ( A - C ) = B ) )
Theorem	pncan 8260	Cancellation law for subtraction. (Contributed by NM, 10-May-2004.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) - B ) = A )
Theorem	pncan2 8261	Cancellation law for subtraction. (Contributed by NM, 17-Apr-2005.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) - A ) = B )
Theorem	pncan3 8262	Subtraction and addition of equals. (Contributed by NM, 14-Mar-2005.)
|- ( ( A e. CC /\ B e. CC ) -> ( A + ( B - A ) ) = B )
Theorem	npcan 8263	Cancellation law for subtraction. (Contributed by NM, 10-May-2004.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( A - B ) + B ) = A )
Theorem	addsubass 8264	Associative-type law for addition and subtraction. (Contributed by NM, 6-Aug-2003.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) - C ) = ( A + ( B - C ) ) )
Theorem	addsub 8265	Law for addition and subtraction. (Contributed by NM, 19-Aug-2001.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) - C ) = ( ( A - C ) + B ) )
Theorem	subadd23 8266	Commutative/associative law for addition and subtraction. (Contributed by NM, 1-Feb-2007.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - B ) + C ) = ( A + ( C - B ) ) )
Theorem	addsub12 8267	Commutative/associative law for addition and subtraction. (Contributed by NM, 8-Feb-2005.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A + ( B - C ) ) = ( B + ( A - C ) ) )
Theorem	2addsub 8268	Law for subtraction and addition. (Contributed by NM, 20-Nov-2005.)
|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( ( A + B ) + C ) - D ) = ( ( ( A + C ) - D ) + B ) )
Theorem	addsubeq4 8269	Relation between sums and differences. (Contributed by Jeff Madsen, 17-Jun-2010.)
|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A + B ) = ( C + D ) <-> ( C - A ) = ( B - D ) ) )
Theorem	pncan3oi 8270	Subtraction and addition of equals. Almost but not exactly the same as pncan3i 8331 and pncan 8260, 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 8366. (Contributed by David A. Wheeler, 11-Oct-2018.)
|- A e. CC   &    |- B e. CC   =>    |- ( ( A + B ) - B ) = A
Theorem	mvrraddi 8271	Move RHS right addition to LHS. (Contributed by David A. Wheeler, 11-Oct-2018.)
|- B e. CC   &    |- C e. CC   &    |- A = ( B + C )   =>    |- ( A - C ) = B
Theorem	mvlladdi 8272	Move LHS left addition to RHS. (Contributed by David A. Wheeler, 11-Oct-2018.)
|- A e. CC   &    |- B e. CC   &    |- ( A + B ) = C   =>    |- B = ( C - A )
Theorem	subid 8273	Subtraction of a number from itself. (Contributed by NM, 8-Oct-1999.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( A e. CC -> ( A - A ) = 0 )
Theorem	subid1 8274	Identity law for subtraction. (Contributed by NM, 9-May-2004.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( A e. CC -> ( A - 0 ) = A )
Theorem	npncan 8275	Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - B ) + ( B - C ) ) = ( A - C ) )
Theorem	nppcan 8276	Cancellation law for subtraction. (Contributed by NM, 1-Sep-2005.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( ( A - B ) + C ) + B ) = ( A + C ) )
Theorem	nnpcan 8277	Cancellation law for subtraction: ((a-b)-c)+b = a-c holds for complex numbers a,b,c. (Contributed by Alexander van der Vekens, 24-Mar-2018.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( ( A - B ) - C ) + B ) = ( A - C ) )
Theorem	nppcan3 8278	Cancellation law for subtraction. (Contributed by Mario Carneiro, 14-Sep-2015.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - B ) + ( C + B ) ) = ( A + C ) )
Theorem	subcan2 8279	Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - C ) = ( B - C ) <-> A = B ) )
Theorem	subeq0 8280	If the difference between two numbers is zero, they are equal. (Contributed by NM, 16-Nov-1999.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( A - B ) = 0 <-> A = B ) )
Theorem	npncan2 8281	Cancellation law for subtraction. (Contributed by Scott Fenton, 21-Jun-2013.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( A - B ) + ( B - A ) ) = 0 )
Theorem	subsub2 8282	Law for double subtraction. (Contributed by NM, 30-Jun-2005.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A - ( B - C ) ) = ( A + ( C - B ) ) )
Theorem	nncan 8283	Cancellation law for subtraction. (Contributed by NM, 21-Jun-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|- ( ( A e. CC /\ B e. CC ) -> ( A - ( A - B ) ) = B )
Theorem	subsub 8284	Law for double subtraction. (Contributed by NM, 13-May-2004.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A - ( B - C ) ) = ( ( A - B ) + C ) )
Theorem	nppcan2 8285	Cancellation law for subtraction. (Contributed by NM, 29-Sep-2005.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - ( B + C ) ) + C ) = ( A - B ) )
Theorem	subsub3 8286	Law for double subtraction. (Contributed by NM, 27-Jul-2005.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A - ( B - C ) ) = ( ( A + C ) - B ) )
Theorem	subsub4 8287	Law for double subtraction. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - B ) - C ) = ( A - ( B + C ) ) )
Theorem	sub32 8288	Swap the second and third terms in a double subtraction. (Contributed by NM, 19-Aug-2005.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - B ) - C ) = ( ( A - C ) - B ) )
Theorem	nnncan 8289	Cancellation law for subtraction. (Contributed by NM, 4-Sep-2005.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - ( B - C ) ) - C ) = ( A - B ) )
Theorem	nnncan1 8290	Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - B ) - ( A - C ) ) = ( C - B ) )
Theorem	nnncan2 8291	Cancellation law for subtraction. (Contributed by NM, 1-Oct-2005.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - C ) - ( B - C ) ) = ( A - B ) )
Theorem	npncan3 8292	Cancellation law for subtraction. (Contributed by Scott Fenton, 23-Jun-2013.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - B ) + ( C - A ) ) = ( C - B ) )
Theorem	pnpcan 8293	Cancellation law for mixed addition and subtraction. (Contributed by NM, 4-Mar-2005.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) - ( A + C ) ) = ( B - C ) )
Theorem	pnpcan2 8294	Cancellation law for mixed addition and subtraction. (Contributed by Scott Fenton, 9-Jun-2006.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + C ) - ( B + C ) ) = ( A - B ) )
Theorem	pnncan 8295	Cancellation law for mixed addition and subtraction. (Contributed by NM, 30-Jun-2005.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) - ( A - C ) ) = ( B + C ) )
Theorem	ppncan 8296	Cancellation law for mixed addition and subtraction. (Contributed by NM, 30-Jun-2005.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) + ( C - B ) ) = ( A + C ) )
Theorem	addsub4 8297	Rearrangement of 4 terms in a mixed addition and subtraction. (Contributed by NM, 4-Mar-2005.)
|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A + B ) - ( C + D ) ) = ( ( A - C ) + ( B - D ) ) )
Theorem	subadd4 8298	Rearrangement of 4 terms in a mixed addition and subtraction. (Contributed by NM, 24-Aug-2006.)
|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A - B ) - ( C - D ) ) = ( ( A + D ) - ( B + C ) ) )
Theorem	sub4 8299	Rearrangement of 4 terms in a subtraction. (Contributed by NM, 23-Nov-2007.)
|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A - B ) - ( C - D ) ) = ( ( A - C ) - ( B - D ) ) )
Theorem	neg0 8300	Minus 0 equals 0. (Contributed by NM, 17-Jan-1997.)
|- -u 0 = 0