P. 85 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 8401-8500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	subadd4 8401	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 8402	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 8403	Minus 0 equals 0. (Contributed by NM, 17-Jan-1997.)
|- -u 0 = 0
Theorem	negid 8404	Addition of a number and its negative. (Contributed by NM, 14-Mar-2005.)
|- ( A e. CC -> ( A + -u A ) = 0 )
Theorem	negsub 8405	Relationship between subtraction and negative. Theorem I.3 of [Apostol] p. 18. (Contributed by NM, 21-Jan-1997.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|- ( ( A e. CC /\ B e. CC ) -> ( A + -u B ) = ( A - B ) )
Theorem	subneg 8406	Relationship between subtraction and negative. (Contributed by NM, 10-May-2004.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( ( A e. CC /\ B e. CC ) -> ( A - -u B ) = ( A + B ) )
Theorem	negneg 8407	A number is equal to the negative of its negative. Theorem I.4 of [Apostol] p. 18. (Contributed by NM, 12-Jan-2002.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( A e. CC -> -u -u A = A )
Theorem	neg11 8408	Negative is one-to-one. (Contributed by NM, 8-Feb-2005.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( ( A e. CC /\ B e. CC ) -> ( -u A = -u B <-> A = B ) )
Theorem	negcon1 8409	Negative contraposition law. (Contributed by NM, 9-May-2004.)
|- ( ( A e. CC /\ B e. CC ) -> ( -u A = B <-> -u B = A ) )
Theorem	negcon2 8410	Negative contraposition law. (Contributed by NM, 14-Nov-2004.)
|- ( ( A e. CC /\ B e. CC ) -> ( A = -u B <-> B = -u A ) )
Theorem	negeq0 8411	A number is zero iff its negative is zero. (Contributed by NM, 12-Jul-2005.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( A e. CC -> ( A = 0 <-> -u A = 0 ) )
Theorem	subcan 8412	Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - B ) = ( A - C ) <-> B = C ) )
Theorem	negsubdi 8413	Distribution of negative over subtraction. (Contributed by NM, 15-Nov-2004.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|- ( ( A e. CC /\ B e. CC ) -> -u ( A - B ) = ( -u A + B ) )
Theorem	negdi 8414	Distribution of negative over addition. (Contributed by NM, 10-May-2004.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|- ( ( A e. CC /\ B e. CC ) -> -u ( A + B ) = ( -u A + -u B ) )
Theorem	negdi2 8415	Distribution of negative over addition. (Contributed by NM, 1-Jan-2006.)
|- ( ( A e. CC /\ B e. CC ) -> -u ( A + B ) = ( -u A - B ) )
Theorem	negsubdi2 8416	Distribution of negative over subtraction. (Contributed by NM, 4-Oct-1999.)
|- ( ( A e. CC /\ B e. CC ) -> -u ( A - B ) = ( B - A ) )
Theorem	neg2sub 8417	Relationship between subtraction and negative. (Contributed by Paul Chapman, 8-Oct-2007.)
|- ( ( A e. CC /\ B e. CC ) -> ( -u A - -u B ) = ( B - A ) )
Theorem	renegcl 8418	Closure law for negative of reals. (Contributed by NM, 20-Jan-1997.)
|- ( A e. RR -> -u A e. RR )
Theorem	renegcli 8419	Closure law for negative of reals. (Note: this inference proof style and the deduction theorem usage in renegcl 8418 is deprecated, but is retained for its demonstration value.) (Contributed by NM, 17-Jan-1997.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
|- A e. RR   =>    |- -u A e. RR
Theorem	resubcli 8420	Closure law for subtraction of reals. (Contributed by NM, 17-Jan-1997.) (Revised by Mario Carneiro, 27-May-2016.)
|- A e. RR   &    |- B e. RR   =>    |- ( A - B ) e. RR
Theorem	resubcl 8421	Closure law for subtraction of reals. (Contributed by NM, 20-Jan-1997.)
|- ( ( A e. RR /\ B e. RR ) -> ( A - B ) e. RR )
Theorem	negreb 8422	The negative of a real is real. (Contributed by NM, 11-Aug-1999.) (Revised by Mario Carneiro, 14-Jul-2014.)
|- ( A e. CC -> ( -u A e. RR <-> A e. RR ) )
Theorem	peano2cnm 8423	"Reverse" second Peano postulate analog for complex numbers: A complex number minus 1 is a complex number. (Contributed by Alexander van der Vekens, 18-Mar-2018.)
|- ( N e. CC -> ( N - 1 ) e. CC )
Theorem	peano2rem 8424	"Reverse" second Peano postulate analog for reals. (Contributed by NM, 6-Feb-2007.)
|- ( N e. RR -> ( N - 1 ) e. RR )
Theorem	negcli 8425	Closure law for negative. (Contributed by NM, 26-Nov-1994.)
|- A e. CC   =>    |- -u A e. CC
Theorem	negidi 8426	Addition of a number and its negative. (Contributed by NM, 26-Nov-1994.)
|- A e. CC   =>    |- ( A + -u A ) = 0
Theorem	negnegi 8427	A number is equal to the negative of its negative. Theorem I.4 of [Apostol] p. 18. (Contributed by NM, 8-Feb-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
|- A e. CC   =>    |- -u -u A = A
Theorem	subidi 8428	Subtraction of a number from itself. (Contributed by NM, 26-Nov-1994.)
|- A e. CC   =>    |- ( A - A ) = 0
Theorem	subid1i 8429	Identity law for subtraction. (Contributed by NM, 29-May-1999.)
|- A e. CC   =>    |- ( A - 0 ) = A
Theorem	negne0bi 8430	A number is nonzero iff its negative is nonzero. (Contributed by NM, 10-Aug-1999.)
|- A e. CC   =>    |- ( A =/= 0 <-> -u A =/= 0 )
Theorem	negrebi 8431	The negative of a real is real. (Contributed by NM, 11-Aug-1999.)
|- A e. CC   =>    |- ( -u A e. RR <-> A e. RR )
Theorem	negne0i 8432	The negative of a nonzero number is nonzero. (Contributed by NM, 30-Jul-2004.)
|- A e. CC   &    |- A =/= 0   =>    |- -u A =/= 0
Theorem	subcli 8433	Closure law for subtraction. (Contributed by NM, 26-Nov-1994.) (Revised by Mario Carneiro, 21-Dec-2013.)
|- A e. CC   &    |- B e. CC   =>    |- ( A - B ) e. CC
Theorem	pncan3i 8434	Subtraction and addition of equals. (Contributed by NM, 26-Nov-1994.)
|- A e. CC   &    |- B e. CC   =>    |- ( A + ( B - A ) ) = B
Theorem	negsubi 8435	Relationship between subtraction and negative. Theorem I.3 of [Apostol] p. 18. (Contributed by NM, 26-Nov-1994.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
|- A e. CC   &    |- B e. CC   =>    |- ( A + -u B ) = ( A - B )
Theorem	subnegi 8436	Relationship between subtraction and negative. (Contributed by NM, 1-Dec-2005.)
|- A e. CC   &    |- B e. CC   =>    |- ( A - -u B ) = ( A + B )
Theorem	subeq0i 8437	If the difference between two numbers is zero, they are equal. (Contributed by NM, 8-May-1999.)
|- A e. CC   &    |- B e. CC   =>    |- ( ( A - B ) = 0 <-> A = B )
Theorem	neg11i 8438	Negative is one-to-one. (Contributed by NM, 1-Aug-1999.)
|- A e. CC   &    |- B e. CC   =>    |- ( -u A = -u B <-> A = B )
Theorem	negcon1i 8439	Negative contraposition law. (Contributed by NM, 25-Aug-1999.)
|- A e. CC   &    |- B e. CC   =>    |- ( -u A = B <-> -u B = A )
Theorem	negcon2i 8440	Negative contraposition law. (Contributed by NM, 25-Aug-1999.)
|- A e. CC   &    |- B e. CC   =>    |- ( A = -u B <-> B = -u A )
Theorem	negdii 8441	Distribution of negative over addition. (Contributed by NM, 28-Jul-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|- A e. CC   &    |- B e. CC   =>    |- -u ( A + B ) = ( -u A + -u B )
Theorem	negsubdii 8442	Distribution of negative over subtraction. (Contributed by NM, 6-Aug-1999.)
|- A e. CC   &    |- B e. CC   =>    |- -u ( A - B ) = ( -u A + B )
Theorem	negsubdi2i 8443	Distribution of negative over subtraction. (Contributed by NM, 1-Oct-1999.)
|- A e. CC   &    |- B e. CC   =>    |- -u ( A - B ) = ( B - A )
Theorem	subaddi 8444	Relationship between subtraction and addition. (Contributed by NM, 26-Nov-1994.) (Revised by Mario Carneiro, 21-Dec-2013.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   =>    |- ( ( A - B ) = C <-> ( B + C ) = A )
Theorem	subadd2i 8445	Relationship between subtraction and addition. (Contributed by NM, 15-Dec-2006.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   =>    |- ( ( A - B ) = C <-> ( C + B ) = A )
Theorem	subaddrii 8446	Relationship between subtraction and addition. (Contributed by NM, 16-Dec-2006.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   &    |- ( B + C ) = A   =>    |- ( A - B ) = C
Theorem	subsub23i 8447	Swap subtrahend and result of subtraction. (Contributed by NM, 7-Oct-1999.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   =>    |- ( ( A - B ) = C <-> ( A - C ) = B )
Theorem	addsubassi 8448	Associative-type law for subtraction and addition. (Contributed by NM, 16-Sep-1999.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   =>    |- ( ( A + B ) - C ) = ( A + ( B - C ) )
Theorem	addsubi 8449	Law for subtraction and addition. (Contributed by NM, 6-Aug-2003.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   =>    |- ( ( A + B ) - C ) = ( ( A - C ) + B )
Theorem	subcani 8450	Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   =>    |- ( ( A - B ) = ( A - C ) <-> B = C )
Theorem	subcan2i 8451	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	pnncani 8452	Cancellation law for mixed addition and subtraction. (Contributed by NM, 14-Jan-2006.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   =>    |- ( ( A + B ) - ( A - C ) ) = ( B + C )
Theorem	addsub4i 8453	Rearrangement of 4 terms in a mixed addition and subtraction. (Contributed by NM, 17-Oct-1999.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   &    |- D e. CC   =>    |- ( ( A + B ) - ( C + D ) ) = ( ( A - C ) + ( B - D ) )
Theorem	0reALT 8454	Alternate proof of 0re 8157. (Contributed by NM, 19-Feb-2005.) (Proof modification is discouraged.) (New usage is discouraged.)
|- 0 e. RR
Theorem	negcld 8455	Closure law for negative. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> -u A e. CC )
Theorem	subidd 8456	Subtraction of a number from itself. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( A - A ) = 0 )
Theorem	subid1d 8457	Identity law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( A - 0 ) = A )
Theorem	negidd 8458	Addition of a number and its negative. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( A + -u A ) = 0 )
Theorem	negnegd 8459	A number is equal to the negative of its negative. Theorem I.4 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> -u -u A = A )
Theorem	negeq0d 8460	A number is zero iff its negative is zero. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( A = 0 <-> -u A = 0 ) )
Theorem	negne0bd 8461	A number is nonzero iff its negative is nonzero. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( A =/= 0 <-> -u A =/= 0 ) )
Theorem	negcon1d 8462	Contraposition law for unary minus. Deduction form of negcon1 8409. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( -u A = B <-> -u B = A ) )
Theorem	negcon1ad 8463	Contraposition law for unary minus. One-way deduction form of negcon1 8409. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A e. CC )   &    |- ( ph -> -u A = B )   =>    |- ( ph -> -u B = A )
Theorem	neg11ad 8464	The negatives of two complex numbers are equal iff they are equal. Deduction form of neg11 8408. Generalization of neg11d 8480. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( -u A = -u B <-> A = B ) )
Theorem	negned 8465	If two complex numbers are unequal, so are their negatives. Contrapositive of neg11d 8480. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> A =/= B )   =>    |- ( ph -> -u A =/= -u B )
Theorem	negne0d 8466	The negative of a nonzero number is nonzero. See also negap0d 8789 which is similar but for apart from zero rather than not equal to zero. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> A =/= 0 )   =>    |- ( ph -> -u A =/= 0 )
Theorem	negrebd 8467	The negative of a real is real. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> -u A e. RR )   =>    |- ( ph -> A e. RR )
Theorem	subcld 8468	Closure law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( A - B ) e. CC )
Theorem	pncand 8469	Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( ( A + B ) - B ) = A )
Theorem	pncan2d 8470	Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( ( A + B ) - A ) = B )
Theorem	pncan3d 8471	Subtraction and addition of equals. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( A + ( B - A ) ) = B )
Theorem	npcand 8472	Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( ( A - B ) + B ) = A )
Theorem	nncand 8473	Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( A - ( A - B ) ) = B )
Theorem	negsubd 8474	Relationship between subtraction and negative. Theorem I.3 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( A + -u B ) = ( A - B ) )
Theorem	subnegd 8475	Relationship between subtraction and negative. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( A - -u B ) = ( A + B ) )
Theorem	subeq0d 8476	If the difference between two numbers is zero, they are equal. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> ( A - B ) = 0 )   =>    |- ( ph -> A = B )
Theorem	subne0d 8477	Two unequal numbers have nonzero difference. See also subap0d 8802 which is the same thing for apartness rather than negated equality. (Contributed by Mario Carneiro, 1-Jan-2017.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> A =/= B )   =>    |- ( ph -> ( A - B ) =/= 0 )
Theorem	subeq0ad 8478	The difference of two complex numbers is zero iff they are equal. Deduction form of subeq0 8383. Generalization of subeq0d 8476. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( ( A - B ) = 0 <-> A = B ) )
Theorem	subne0ad 8479	If the difference of two complex numbers is nonzero, they are unequal. Converse of subne0d 8477. Contrapositive of subeq0bd 8536. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> ( A - B ) =/= 0 )   =>    |- ( ph -> A =/= B )
Theorem	neg11d 8480	If the difference between two numbers is zero, they are equal. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> -u A = -u B )   =>    |- ( ph -> A = B )
Theorem	negdid 8481	Distribution of negative over addition. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> -u ( A + B ) = ( -u A + -u B ) )
Theorem	negdi2d 8482	Distribution of negative over addition. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> -u ( A + B ) = ( -u A - B ) )
Theorem	negsubdid 8483	Distribution of negative over subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> -u ( A - B ) = ( -u A + B ) )
Theorem	negsubdi2d 8484	Distribution of negative over subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> -u ( A - B ) = ( B - A ) )
Theorem	neg2subd 8485	Relationship between subtraction and negative. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( -u A - -u B ) = ( B - A ) )
Theorem	subaddd 8486	Relationship between subtraction and addition. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A - B ) = C <-> ( B + C ) = A ) )
Theorem	subadd2d 8487	Relationship between subtraction and addition. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A - B ) = C <-> ( C + B ) = A ) )
Theorem	addsubassd 8488	Associative-type law for subtraction and addition. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A + B ) - C ) = ( A + ( B - C ) ) )
Theorem	addsubd 8489	Law for subtraction and addition. (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	subadd23d 8490	Commutative/associative law for addition and subtraction. (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	addsub12d 8491	Commutative/associative law for addition and subtraction. (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	npncand 8492	Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A - B ) + ( B - C ) ) = ( A - C ) )
Theorem	nppcand 8493	Cancellation law for subtraction. (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	nppcan2d 8494	Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A - ( B + C ) ) + C ) = ( A - B ) )
Theorem	nppcan3d 8495	Cancellation law for subtraction. (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	subsubd 8496	Law for double subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( A - ( B - C ) ) = ( ( A - B ) + C ) )
Theorem	subsub2d 8497	Law for double subtraction. (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	subsub3d 8498	Law for double subtraction. (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	subsub4d 8499	Law for double subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A - B ) - C ) = ( A - ( B + C ) ) )
Theorem	sub32d 8500	Swap the second and third terms in a double subtraction. (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 ) )