Metamath Proof Explorer

Theorem fldidom

Description: A field is an integral domain. (Contributed by Mario Carneiro, 29-Mar-2015) (Proof shortened by SN, 11-Nov-2024)

		Ref	Expression
	Assertion	fldidom	$⊢ R \in Field \to R \in IDomn$

Step	Hyp	Ref	Expression
1		drngdomn	$⊢ R \in DivRing \to R \in Domn$
2	1	anim1ci	$⊢ (R \in DivRing \land R \in CRing) \to (R \in CRing \land R \in Domn)$
3		isfld	$⊢ R \in Field \leftrightarrow (R \in DivRing \land R \in CRing)$
4		isidom	$⊢ R \in IDomn \leftrightarrow (R \in CRing \land R \in Domn)$
5	2 3 4	3imtr4i	$⊢ R \in Field \to R \in IDomn$