Theorem resubidaddid1lem

Description: Lemma for resubidaddid1 . A special case of npncan . (Contributed by Steven Nguyen, 8-Jan-2023)

	Ref	Expression
Hypotheses	resubidaddid1lem.a	|- ( ph -> A e. RR )
	resubidaddid1lem.b	|- ( ph -> B e. RR )
	resubidaddid1lem.c	|- ( ph -> C e. RR )
	resubidaddid1lem.1	|- ( ph -> ( A -R B ) = ( B -R C ) )
Assertion	resubidaddid1lem	|- ( ph -> ( ( A -R B ) + ( B -R C ) ) = ( A -R C ) )

Proof

Step	Hyp	Ref	Expression
1		resubidaddid1lem.a	|- ( ph -> A e. RR )
2		resubidaddid1lem.b	|- ( ph -> B e. RR )
3		resubidaddid1lem.c	|- ( ph -> C e. RR )
4		resubidaddid1lem.1	|- ( ph -> ( A -R B ) = ( B -R C ) )
5		rersubcl	|- ( ( A e. RR /\ B e. RR ) -> ( A -R B ) e. RR )
6	1 2 5	syl2anc	|- ( ph -> ( A -R B ) e. RR )
7		rersubcl	|- ( ( B e. RR /\ C e. RR ) -> ( B -R C ) e. RR )
8	2 3 7	syl2anc	|- ( ph -> ( B -R C ) e. RR )
9	6 8	readdcld	|- ( ph -> ( ( A -R B ) + ( B -R C ) ) e. RR )
10	4	eqcomd	|- ( ph -> ( B -R C ) = ( A -R B ) )
11	2 3 6	resubaddd	|- ( ph -> ( ( B -R C ) = ( A -R B ) <-> ( C + ( A -R B ) ) = B ) )
12	10 11	mpbid	|- ( ph -> ( C + ( A -R B ) ) = B )
13	12	oveq1d	|- ( ph -> ( ( C + ( A -R B ) ) + ( B -R C ) ) = ( B + ( B -R C ) ) )
14	3	recnd	|- ( ph -> C e. CC )
15	6	recnd	|- ( ph -> ( A -R B ) e. CC )
16	8	recnd	|- ( ph -> ( B -R C ) e. CC )
17	14 15 16	addassd	|- ( ph -> ( ( C + ( A -R B ) ) + ( B -R C ) ) = ( C + ( ( A -R B ) + ( B -R C ) ) ) )
18	1 2 8	resubaddd	|- ( ph -> ( ( A -R B ) = ( B -R C ) <-> ( B + ( B -R C ) ) = A ) )
19	4 18	mpbid	|- ( ph -> ( B + ( B -R C ) ) = A )
20	13 17 19	3eqtr3d	|- ( ph -> ( C + ( ( A -R B ) + ( B -R C ) ) ) = A )
21	3 9 20	reladdrsub	|- ( ph -> ( ( A -R B ) + ( B -R C ) ) = ( A -R C ) )