Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ablgrp | Unicode version |
Description: An Abelian group is a group. (Contributed by NM, 26-Aug-2011.) |
Ref | Expression |
---|---|
ablgrp |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | isabl 12888 | . 2 CMnd | |
2 | 1 | simplbi 274 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wcel 2146 cgrp 12738 CMndccmn 12884 cabl 12885 |
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 709 ax-5 1445 ax-7 1446 ax-gen 1447 ax-ie1 1491 ax-ie2 1492 ax-8 1502 ax-10 1503 ax-11 1504 ax-i12 1505 ax-bndl 1507 ax-4 1508 ax-17 1524 ax-i9 1528 ax-ial 1532 ax-i5r 1533 ax-ext 2157 |
This theorem depends on definitions: df-bi 117 df-tru 1356 df-nf 1459 df-sb 1761 df-clab 2162 df-cleq 2168 df-clel 2171 df-nfc 2306 df-v 2737 df-in 3133 df-abl 12887 |
This theorem is referenced by: ablgrpd 12890 ablinvadd 12909 ablsub2inv 12910 ablsubadd 12911 ablsub4 12912 abladdsub4 12913 abladdsub 12914 ablpncan2 12915 ablpncan3 12916 ablsubsub 12917 ablsubsub4 12918 ablpnpcan 12919 ablnncan 12920 ablnnncan 12922 ablnnncan1 12923 ablsubsub23 12924 |
Copyright terms: Public domain | W3C validator |