Description: Commutative/associative law for commutative ring. (Contributed by Thierry Arnoux, 14-Jan-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cringm4.1 | ||
cringm4.2 | |||
Assertion | cringm4 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cringm4.1 | ||
2 | cringm4.2 | ||
3 | eqid | ||
4 | 3 | crngmgp | |
5 | 3 1 | mgpbas | |
6 | 3 2 | mgpplusg | |
7 | 5 6 | cmn4 | |
8 | 4 7 | syl3an1 |