Metamath Proof Explorer


Theorem sn-addcan2d

Description: addcan2d without ax-mulcom . (Contributed by SN, 5-May-2024)

Ref Expression
Hypotheses sn-addcan2d.a φ A
sn-addcan2d.b φ B
sn-addcan2d.c φ C
Assertion sn-addcan2d φ A + C = B + C A = B

Proof

Step Hyp Ref Expression
1 sn-addcan2d.a φ A
2 sn-addcan2d.b φ B
3 sn-addcan2d.c φ C
4 sn-negex C x C + x = 0
5 3 4 syl φ x C + x = 0
6 oveq1 A + C = B + C A + C + x = B + C + x
7 1 adantr φ x C + x = 0 A
8 3 adantr φ x C + x = 0 C
9 simprl φ x C + x = 0 x
10 7 8 9 addassd φ x C + x = 0 A + C + x = A + C + x
11 simprr φ x C + x = 0 C + x = 0
12 11 oveq2d φ x C + x = 0 A + C + x = A + 0
13 sn-addid1 A A + 0 = A
14 7 13 syl φ x C + x = 0 A + 0 = A
15 10 12 14 3eqtrd φ x C + x = 0 A + C + x = A
16 2 adantr φ x C + x = 0 B
17 16 8 9 addassd φ x C + x = 0 B + C + x = B + C + x
18 11 oveq2d φ x C + x = 0 B + C + x = B + 0
19 sn-addid1 B B + 0 = B
20 16 19 syl φ x C + x = 0 B + 0 = B
21 17 18 20 3eqtrd φ x C + x = 0 B + C + x = B
22 15 21 eqeq12d φ x C + x = 0 A + C + x = B + C + x A = B
23 6 22 syl5ib φ x C + x = 0 A + C = B + C A = B
24 oveq1 A = B A + C = B + C
25 23 24 impbid1 φ x C + x = 0 A + C = B + C A = B
26 5 25 rexlimddv φ A + C = B + C A = B