Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∧ w3a 1085
= wceq 1539 ∈
wcel 2104 ‘cfv 6542
(class class class)co 7411 Basecbs 17148
+gcplusg 17201 Grpcgrp 18855
Ringcrg 20127 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911
ax-6 1969 ax-7 2009 ax-8 2106
ax-9 2114 ax-ext 2701 ax-nul 5305 |
This theorem depends on definitions:
df-bi 206 df-an 395
df-or 844 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1780 df-sb 2066 df-clab 2708 df-cleq 2722 df-clel 2808 df-ne 2939 df-ral 3060 df-rex 3069 df-rab 3431 df-v 3474 df-sbc 3777 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-if 4528 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-br 5148 df-iota 6494 df-fv 6550 df-ov 7414 df-mgm 18565 df-sgrp 18644 df-mnd 18660 df-grp 18858 df-ring 20129 |
This theorem is referenced by: ringcomlem
20167 ringcom
20168 ringlghm
20200 ringrghm
20201 imasring
20218 qusring2
20222 cntzsubr
20496 srngadd
20608 issrngd
20612 lmodprop2d
20678 prdslmodd
20724 ip2subdi
21416 psrlmod
21740 mpfind
21889 coe1add
22006 mat1ghm
22205 scmatghm
22255 mdetrlin2
22329 mdetunilem5
22338 cpmatacl
22438 mdegaddle
25827 deg1addle2
25855 deg1add
25856 ply1divex
25889 frobrhm
32652 rhmpreimaidl
32811 deg1addlt
32945 dvhlveclem
40282 baerlem3lem1
40881 mendlmod
42237 cznrng
46941 lmod1lem3
47257 |