Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 = wceq 1534
∈ wcel 2099 ‘cfv 6548 (class class class)co 7420
Basecbs 17180 +gcplusg 17233 Grpcgrp 18890 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906
ax-6 1964 ax-7 2004 ax-8 2101
ax-9 2109 ax-ext 2699 ax-nul 5306 |
This theorem depends on definitions:
df-bi 206 df-an 396
df-or 847 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-sb 2061 df-clab 2706 df-cleq 2720 df-clel 2806 df-ne 2938 df-ral 3059 df-rex 3068 df-rab 3430 df-v 3473 df-sbc 3777 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4324 df-if 4530 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4909 df-br 5149 df-iota 6500 df-fv 6556 df-ov 7423 df-mgm 18600 df-sgrp 18679 df-mnd 18695 df-grp 18893 |
This theorem is referenced by: grpraddf1o
18970 dfgrp3
18995 xpsinv
19016 xpsgrpsub
19017 nmzsubg
19120 eqger
19133 conjnmz
19206 ghmquskerlem3
19237 lringuplu
20481 rnglidl1
21128 rngqiprngimfo
21191 rngqiprngfulem3
21203 psdmul
22090 evls1addd
22290 evls1maprhm
22295 cphpyth
25157 rlocaddval
32995 rloccring
32997 rlocf1
33000 ghmqusnsg
33144 ply1degltlss
33267 q1pdir
33273 r1pcyc
33277 r1padd1
33278 r1plmhm
33280 algextdeglem8
33392 aks6d1c1p3
41581 grpcominv1
41748 rhmmpl
41786 mplmapghm
41789 evlsmaprhm
41803 evladdval
41808 selvadd
41821 |