Theorem subrgcccrng

Description: A subring of the complex numbers is a commutative ring. (Contributed by AV, 26-Oct-2026)

	Ref	Expression
Hypotheses	subrgcccrng.r	|- R = ( CCfld |`s S )
	subrgcccrng.s	|- S e. ( SubRing ` CCfld )
Assertion	subrgcccrng	|- R e. CRing

Proof

Step	Hyp	Ref	Expression
1		subrgcccrng.r	|- R = ( CCfld |`s S )
2		subrgcccrng.s	|- S e. ( SubRing ` CCfld )
3		cncrng	|- CCfld e. CRing
4	1	subrgcrng	|- ( ( CCfld e. CRing /\ S e. ( SubRing ` CCfld ) ) -> R e. CRing )
5	3 2 4	mp2an	|- R e. CRing