Metamath Proof Explorer

Theorem crngprmringdom

Description: A commutative ring is a prime ring if and only if it is a domain. (Contributed by AV, 27-Jun-2026)

Ref Expression
Assertion crngprmringdom 
|- ( R e. CRing -> ( R e. PrmRing <-> R e. Domn ) )

Proof

Step Hyp Ref Expression
1 crngprmringidom 
 |-  ( R e. CRing -> ( R e. PrmRing <-> R e. IDomn ) )
2 isidom 
 |-  ( R e. IDomn <-> ( R e. CRing /\ R e. Domn ) )
3 2 baib 
 |-  ( R e. CRing -> ( R e. IDomn <-> R e. Domn ) )
4 1 3 bitrd 
 |-  ( R e. CRing -> ( R e. PrmRing <-> R e. Domn ) )