Metamath Proof Explorer


Theorem sn-addid1

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

Ref Expression
Assertion sn-addid1 A A + 0 = A

Proof

Step Hyp Ref Expression
1 sn-negex2 A x x + A = 0
2 simprr A x x + A = 0 x + A = 0
3 2 oveq1d A x x + A = 0 x + A + 0 = 0 + 0
4 sn-00id 0 + 0 = 0
5 3 4 eqtrdi A x x + A = 0 x + A + 0 = 0
6 simprl A x x + A = 0 x
7 simpl A x x + A = 0 A
8 0cnd A x x + A = 0 0
9 6 7 8 addassd A x x + A = 0 x + A + 0 = x + A + 0
10 2 5 9 3eqtr2rd A x x + A = 0 x + A + 0 = x + A
11 7 8 addcld A x x + A = 0 A + 0
12 6 11 7 sn-addcand A x x + A = 0 x + A + 0 = x + A A + 0 = A
13 10 12 mpbid A x x + A = 0 A + 0 = A
14 1 13 rexlimddv A A + 0 = A