Metamath Proof Explorer

Theorem flddmn

Description: Obsolete theorem, use fldidom instead. A field is a domain. (Contributed by Jeff Madsen, 10-Jun-2010) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

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$