P. 70 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 6901-7000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	mul31 6901	Commutative/associative law. (Contributed by Scott Fenton, 3-Jan-2013.)
|- ((A e. CC /\ B e. CC /\ C e. CC) -> ((A x. B) x. C) = (( C x. B) x. A))
Theorem	mul4 6902	Rearrangement of 4 factors. (Contributed by NM, 8-Oct-1999.)
|- (((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	muladd11 6903	A simple product of sums expansion. (Contributed by NM, 21-Feb-2005.)
|- ((A e. CC /\ B e. CC) -> (( 1 + A) x. ( 1 + B)) = (( 1 + A) + (B + (A x. B))))
Theorem	1p1times 6904	Two times a number. (Contributed by NM, 18-May-1999.) (Revised by Mario Carneiro, 27-May-2016.)
|- (A e. CC -> (( 1 + 1) x. A) = (A + A))
Theorem	peano2cn 6905	A theorem for complex numbers analogous the second Peano postulate peano2 4261. (Contributed by NM, 17-Aug-2005.)
|- (A e. CC -> (A + 1) e. CC)
Theorem	peano2re 6906	A theorem for reals analogous the second Peano postulate peano2 4261. (Contributed by NM, 5-Jul-2005.)
|- (A e. RR -> (A + 1) e. RR)
Theorem	addcom 6907	Addition commutes. (Contributed by Jim Kingdon, 17-Jan-2020.)
|- ((A e. CC /\ B e. CC) -> (A + B) = (B + A))
Theorem	addid1 6908	0 is an additive identity. (Contributed by Jim Kingdon, 16-Jan-2020.)
|- (A e. CC -> (A + 0) = A)
Theorem	addid2 6909	0 is a left identity for addition. (Contributed by Scott Fenton, 3-Jan-2013.)
|- (A e. CC -> ( 0 + A) = A)
Theorem	readdcan 6910	Cancellation law for addition over the reals. (Contributed by Scott Fenton, 3-Jan-2013.)
|- ((A e. RR /\ B e. RR /\ C e. RR) -> (( C + A) = ( C + B) <-> A = B))
Theorem	00id 6911	0 is its own additive identity. (Contributed by Scott Fenton, 3-Jan-2013.)
|- ( 0 + 0) = 0
Theorem	addid1i 6912	0 is an additive identity. (Contributed by NM, 23-Nov-1994.) (Revised by Scott Fenton, 3-Jan-2013.)
|- A e. CC   =>   |- (A + 0) = A
Theorem	addid2i 6913	0 is a left identity for addition. (Contributed by NM, 3-Jan-2013.)
|- A e. CC   =>   |- ( 0 + A) = A
Theorem	addcomi 6914	Addition commutes. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.)
|- A e. CC   &   |- B e. CC   =>   |- (A + B) = (B + A)
Theorem	addcomli 6915	Addition commutes. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- A e. CC   &   |- B e. CC   &   |- (A + B) = C   =>   |- (B + A) = C
Theorem	mul12i 6916	Commutative/associative law that swaps the first two factors in a triple product. (Contributed by NM, 11-May-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|- A e. CC   &   |- B e. CC   &   |- C e. CC   =>   |- (A x. (B x. C)) = (B x. (A x. C))
Theorem	mul32i 6917	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 6918	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	addid1d 6919	0 is an additive identity. (Contributed by Mario Carneiro, 27-May-2016.)
|- (ph -> A e. CC)   =>   |- (ph -> (A + 0) = A)
Theorem	addid2d 6920	0 is a left identity for addition. (Contributed by Mario Carneiro, 27-May-2016.)
|- (ph -> A e. CC)   =>   |- (ph -> ( 0 + A) = A)
Theorem	addcomd 6921	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 6922	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 6923	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 6924	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 6925	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)))
3.3  Real and complex numbers - basic operations
3.3.1  Addition
Theorem	add12 6926	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 6927	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 6928	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 6929	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 6930	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 6931	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 6932	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 6933	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 6934	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 6935	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 6936	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 6937	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 6938	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)))
3.3.2  Subtraction
Syntax	cmin 6939	Extend class notation to include subtraction.
class -
Syntax	cneg 6940	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 6939 ( -) to prevent syntax ambiguity. For example, looking at the syntax definition co 5455, 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, "( -uA - B) " is unambiguous.
class -uA
Definition	df-sub 6941*	Define subtraction. Theorem subval 6960 shows its value (and describes how this definition works), theorem subaddi 7054 relates it to addition, and theorems subcli 7043 and resubcli 7030 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 6942	Define the negative of a number (unary minus). We use different symbols for unary minus ( -u) and subtraction ( -) to prevent syntax ambiguity. See cneg 6940 for a discussion of this. (Contributed by NM, 10-Feb-1995.)
|- -uA = ( 0 - A)
Theorem	cnegexlem1 6943	Addition cancellation of a real number from two complex numbers. Lemma for cnegex 6946. (Contributed by Eric Schmidt, 22-May-2007.)
|- ((A e. RR /\ B e. CC /\ C e. CC) -> ((A + B) = (A + C) <-> B = C))
Theorem	cnegexlem2 6944	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 6946. (Contributed by Eric Schmidt, 22-May-2007.)
|- E.y e. RR ( _i x. y) e. RR
Theorem	cnegexlem3 6945*	Existence of real number difference. Lemma for cnegex 6946. (Contributed by Eric Schmidt, 22-May-2007.)
|- (( b e. RR /\ y e. RR) -> E. c e. RR ( b + c) = y)
Theorem	cnegex 6946*	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 6947*	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 6948	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 6949	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 6950	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 6951	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 6952	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 6953	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 6954	Cancelling a term on the left-hand side of a sum in an equality. Consequence of addcand 6952. (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 6955	Cancelling a term on the right-hand side of a sum in an equality. Consequence of addcan2d 6953. (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 6956	Introducing a term on the left-hand side of a sum in a negated equality. Contrapositive of addcanad 6954. Consequence of addcand 6952. (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 6957	Introducing a term on the right-hand side of a sum in a negated equality. Contrapositive of addcan2ad 6955. Consequence of addcan2d 6953. (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 6958	Alternate proof of 0cn 6777. (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 6959*	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 6960*	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 6961	Equality theorem for negatives. (Contributed by NM, 10-Feb-1995.)
|- (A = B -> -uA = -uB)
Theorem	negeqi 6962	Equality inference for negatives. (Contributed by NM, 14-Feb-1995.)
|- A = B   =>   |- -uA = -uB
Theorem	negeqd 6963	Equality deduction for negatives. (Contributed by NM, 14-May-1999.)
|- (ph -> A = B)   =>   |- (ph -> -uA = -uB)
Theorem	nfnegd 6964	Deduction version of nfneg 6965. (Contributed by NM, 29-Feb-2008.) (Revised by Mario Carneiro, 15-Oct-2016.)
|- (ph -> F/_xA)   =>   |- (ph -> F/_x -uA)
Theorem	nfneg 6965	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/_xA   =>   |- F/_x -uA
Theorem	csbnegg 6966	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 ]_ -uB = -u [_A / x ]_B)
Theorem	subcl 6967	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 6968	Closure law for negative. (Contributed by NM, 6-Aug-2003.)
|- (A e. CC -> -uA e. CC)
Theorem	negicn 6969	-u _i is a complex number (common case). (Contributed by David A. Wheeler, 7-Dec-2018.)
|- -u _i e. CC
Theorem	subf 6970	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 6971	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 6972	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 6973	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 6974	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 6975	Cancellation law for subtraction. (Contributed by NM, 17-Apr-2005.)
|- ((A e. CC /\ B e. CC) -> ((A + B) - A) = B)
Theorem	pncan3 6976	Subtraction and addition of equals. (Contributed by NM, 14-Mar-2005.)
|- ((A e. CC /\ B e. CC) -> (A + (B - A)) = B)
Theorem	npcan 6977	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 6978	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 6979	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 6980	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 6981	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 6982	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 6983	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 6984	Subtraction and addition of equals. Almost but not exactly the same as pncan3i 7044 and pncan 6974, 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 7079. (Contributed by David A. Wheeler, 11-Oct-2018.)
|- A e. CC   &   |- B e. CC   =>   |- ((A + B) - B) = A
Theorem	mvlladdi 6985	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 6986	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 6987	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 6988	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 6989	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 6990	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 6991	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 6992	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 6993	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 6994	Cancellation law for subtraction. (Contributed by Scott Fenton, 21-Jun-2013.)
|- ((A e. CC /\ B e. CC) -> ((A - B) + (B - A)) = 0)
Theorem	subsub2 6995	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 6996	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 6997	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 6998	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 6999	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 7000	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)))