Theorem fldidom

Description: A field is an integral domain. (Contributed by Mario Carneiro, 29-Mar-2015)

	Ref	Expression
Assertion	fldidom	|- ( R e. Field -> R e. IDomn )

Proof

Step	Hyp	Ref	Expression
1		isfld	|- ( R e. Field <-> ( R e. DivRing /\ R e. CRing ) )
2	1	simprbi	|- ( R e. Field -> R e. CRing )
3	1	simplbi	|- ( R e. Field -> R e. DivRing )
4		drngdomn	|- ( R e. DivRing -> R e. Domn )
5	3 4	syl	|- ( R e. Field -> R e. Domn )
6		isidom	|- ( R e. IDomn <-> ( R e. CRing /\ R e. Domn ) )
7	2 5 6	sylanbrc	|- ( R e. Field -> R e. IDomn )