Colors of
variables: wff
setvar class |
Syntax hints:
↔ wb 205 ∧ wa 397
∈ wcel 2107 CRingccrg 20057
Domncdomn 20896 IDomncidom 20897 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914
ax-6 1972 ax-7 2012 ax-8 2109
ax-9 2117 ax-ext 2704 |
This theorem depends on definitions:
df-bi 206 df-an 398
df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-v 3477 df-in 3956 df-idom 20901 |
This theorem is referenced by: fldidom
20923 fldidomOLD
20924 fiidomfld
20927 znfld
21116 znidomb
21117 recvsOLD
24663 ply1idom
25642 fta1glem1
25683 fta1glem2
25684 fta1g
25685 fta1b
25687 lgsqrlem1
26849 lgsqrlem2
26850 lgsqrlem3
26851 lgsqrlem4
26852 dvdsruasso
32490 qsidomlem1
32571 qsidomlem2
32572 idomrootle
41937 idomodle
41938 proot1mul
41941 proot1hash
41942 |