Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > crngringd | Structured version Visualization version GIF version |
Description: A commutative ring is a ring. (Contributed by SN, 16-May-2024.) |
Ref | Expression |
---|---|
crngringd.1 | ⊢ (𝜑 → 𝑅 ∈ CRing) |
Ref | Expression |
---|---|
crngringd | ⊢ (𝜑 → 𝑅 ∈ Ring) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | crngringd.1 | . 2 ⊢ (𝜑 → 𝑅 ∈ CRing) | |
2 | crngring 19806 | . 2 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → 𝑅 ∈ Ring) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2110 Ringcrg 19794 CRingccrg 19795 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2015 ax-8 2112 ax-9 2120 ax-ext 2711 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1545 df-fal 1555 df-ex 1787 df-sb 2072 df-clab 2718 df-cleq 2732 df-clel 2818 df-rab 3075 df-v 3433 df-dif 3895 df-un 3897 df-in 3899 df-ss 3909 df-nul 4263 df-if 4466 df-sn 4568 df-pr 4570 df-op 4574 df-uni 4846 df-br 5080 df-iota 6390 df-fv 6440 df-cring 19797 |
This theorem is referenced by: crnggrpd 19808 asclrhm 21105 evlslem1 21303 recvs 24320 frobrhm 31494 znfermltl 31571 idlsrgmulrssin 31667 ply1fermltl 31679 zarclsun 31829 zarmxt1 31839 zarcmplem 31840 pwsgprod 40278 mplascl0 40279 evl0 40280 evlsval3 40281 evlsbagval 40284 evlsexpval 40285 mhphf 40294 mhphf4 40297 |
Copyright terms: Public domain | W3C validator |