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 ~=r S -> ( R e. CRing <-> S e. CRing ) )

Proof

Step Hyp Ref Expression
1 riccrng1 
 |-  ( ( R ~=r S /\ R e. CRing ) -> S e. CRing )
2 ricsym 
 |-  ( R ~=r S -> S ~=r R )
3 riccrng1 
 |-  ( ( S ~=r R /\ S e. CRing ) -> R e. CRing )
4 2 3 sylan 
 |-  ( ( R ~=r S /\ S e. CRing ) -> R e. CRing )
5 1 4 impbida 
 |-  ( R ~=r S -> ( R e. CRing <-> S e. CRing ) )