Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∈ wcel 2106
RingOpscrngo 36848 Com2ccm2 36943
CRingOpsccring 36947 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913
ax-6 1971 ax-7 2011 ax-8 2108
ax-9 2116 ax-ext 2703 |
This theorem depends on definitions:
df-bi 206 df-an 397
df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2710 df-cleq 2724 df-clel 2810 df-v 3476 df-in 3955 df-crngo 36948 |
This theorem is referenced by: crngm23
36956 crngm4
36957 crngohomfo
36960 isidlc
36969 dmnrngo
37011 prnc
37021 isfldidl
37022 isfldidl2
37023 ispridlc
37024 pridlc3
37027 isdmn3
37028 |