flddmn

		Ref	Expression
	Assertion	flddmn	$⊢ K \in Fld \to K \in Dmn$

Step	Hyp	Ref	Expression
1		divrngpr	$⊢ K \in DivRingOps \to K \in PrRing$
2	1	anim1i	$⊢ (K \in DivRingOps \land K \in CRingOps) \to (K \in PrRing \land K \in CRingOps)$
3		isfld2	$⊢ K \in Fld \leftrightarrow (K \in DivRingOps \land K \in CRingOps)$
4		isdmn2	$⊢ K \in Dmn \leftrightarrow (K \in PrRing \land K \in CRingOps)$
5	2 3 4	3imtr4i	$⊢ K \in Fld \to K \in Dmn$

Metamath Proof Explorer