Metamath Proof Explorer

Theorem flddmn

Description: A field is a domain. (Contributed by Jeff Madsen, 10-Jun-2010)

Ref Expression
Assertion flddmn 
|- ( K e. Fld -> K e. Dmn )

Proof

Step Hyp Ref Expression
1 divrngpr 
 |-  ( K e. DivRingOps -> K e. PrRing )
2 1 anim1i 
 |-  ( ( K e. DivRingOps /\ K e. CRingOps ) -> ( K e. PrRing /\ K e. CRingOps ) )
3 isfld2 
 |-  ( K e. Fld <-> ( K e. DivRingOps /\ K e. CRingOps ) )
4 isdmn2 
 |-  ( K e. Dmn <-> ( K e. PrRing /\ K e. CRingOps ) )
5 2 3 4 3imtr4i 
 |-  ( K e. Fld -> K e. Dmn )