| Colors of
variables: wff set class |
| Syntax hints:
∧ wa 104 = wceq 1364
∈ wcel 2160 ‘cfv 5231 ℕcn 8938
2c2 8989 ndxcnx 12483
Slot cslot 12485 +gcplusg 12561 |
| This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 710
ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-13 2162 ax-14 2163 ax-ext 2171 ax-sep 4136 ax-pow 4189 ax-pr 4224 ax-un 4448 ax-cnex 7921 ax-resscn 7922 ax-1re 7924 ax-addrcl 7927 |
| This theorem depends on definitions:
df-bi 117 df-3an 982 df-tru 1367 df-nf 1472 df-sb 1774 df-eu 2041 df-mo 2042 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-ral 2473 df-rex 2474 df-v 2754 df-sbc 2978 df-un 3148 df-in 3150 df-ss 3157 df-pw 3592 df-sn 3613 df-pr 3614 df-op 3616 df-uni 3825 df-int 3860 df-br 4019 df-opab 4080 df-mpt 4081 df-id 4308 df-xp 4647 df-rel 4648 df-cnv 4649 df-co 4650 df-dm 4651 df-rn 4652 df-res 4653 df-iota 5193 df-fun 5233 df-fv 5239 df-ov 5894 df-inn 8939 df-2 8997 df-ndx 12489 df-slot 12490 df-plusg 12574 |
| This theorem is referenced by: ressplusgd
12612 rngplusgg
12620 srngplusgd
12631 lmodplusgd
12649 ipsaddgd
12661 topgrpplusgd
12681 imasex
12754 imasival
12755 imasbas
12756 imasplusg
12757 imasaddfn
12766 imasaddval
12767 imasaddf
12768 qusaddval
12783 qusaddf
12784 ismgm
12805 plusfvalg
12811 plusffng
12813 issgrp
12838 ismnddef
12851 grppropstrg
12936 grpsubval
12962 mulgval
13036 mulgfng
13038 mulg1
13041 mulgnnp1
13042 mulgnndir
13063 subgintm
13109 isnsg
13113 fnmgp
13243 mgpvalg
13244 mgpplusgg
13245 mgpex
13246 mgpbasg
13247 mgpscag
13248 mgptsetg
13249 mgpdsg
13251 mgpress
13252 isrng
13255 issrg
13286 isring
13321 ring1
13378 oppraddg
13393 islmod
13574 rmodislmod
13634 lsssn0
13653 lss1d
13666 lssintclm
13667 sraaddgg
13723 cnfldadd
13836 |
