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	⊢ ( 𝑅 ∈ CRing → ( 𝑅 ∈ PrmRing ↔ 𝑅 ∈ Domn ) )

Proof

Step	Hyp	Ref	Expression
1		crngprmringidom	⊢ ( 𝑅 ∈ CRing → ( 𝑅 ∈ PrmRing ↔ 𝑅 ∈ IDomn ) )
2		isidom	⊢ ( 𝑅 ∈ IDomn ↔ ( 𝑅 ∈ CRing ∧ 𝑅 ∈ Domn ) )
3	2	baib	⊢ ( 𝑅 ∈ CRing → ( 𝑅 ∈ IDomn ↔ 𝑅 ∈ Domn ) )
4	1 3	bitrd	⊢ ( 𝑅 ∈ CRing → ( 𝑅 ∈ PrmRing ↔ 𝑅 ∈ Domn ) )