Metamath Proof Explorer


Theorem sn-negex2

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

Ref Expression
Assertion sn-negex2 A b b + A = 0

Proof

Step Hyp Ref Expression
1 sn-negex12 A b A + b = 0 b + A = 0
2 simpr A + b = 0 b + A = 0 b + A = 0
3 2 reximi b A + b = 0 b + A = 0 b b + A = 0
4 1 3 syl A b b + A = 0