Metamath Proof Explorer


Theorem sn-addcand

Description: addcand without ax-mulcom . Note how the proof is almost identical to addcan . (Contributed by SN, 5-May-2024)

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

Proof

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