Metamath Proof Explorer


Theorem riccrng

Description: A ring is commutative if and only if an isomorphic ring is commutative. (Contributed by SN, 10-Jan-2025)

Ref Expression
Assertion riccrng R 𝑟 S R CRing S CRing

Proof

Step Hyp Ref Expression
1 riccrng1 R 𝑟 S R CRing S CRing
2 ricsym R 𝑟 S S 𝑟 R
3 riccrng1 S 𝑟 R S CRing R CRing
4 2 3 sylan R 𝑟 S S CRing R CRing
5 1 4 impbida R 𝑟 S R CRing S CRing