Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  isidom Structured version   Unicode version

Theorem isidom 16365
 Description: An integral domain is a commutative domain. (Contributed by Mario Carneiro, 17-Jun-2015.)
Assertion
Ref Expression
isidom IDomn Domn

Proof of Theorem isidom
StepHypRef Expression
1 df-idom 16346 . 2 IDomn Domn
21elin2 3532 1 IDomn Domn
 Colors of variables: wff set class Syntax hints:   wb 178   wa 360   wcel 1726  ccrg 15662  Domncdomn 16341  IDomncidom 16342 This theorem is referenced by:  fldidom  16366  fiidomfld  16369  znfld  16842  znidomb  16843  ply1idom  20048  fta1glem1  20089  fta1glem2  20090  fta1g  20091  fta1b  20093  lgsqrlem1  21126  lgsqrlem2  21127  lgsqrlem3  21128  lgsqrlem4  21129  idomrootle  27489  idomodle  27490  proot1mul  27493  proot1hash  27497 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2418 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-v 2959  df-in 3328  df-idom 16346
 Copyright terms: Public domain W3C validator