| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > grpcl | Unicode version | ||
| Description: Closure of the operation of a group. (Contributed by NM, 14-Aug-2011.) |
| Ref | Expression |
|---|---|
| grpcl.b |
|
| grpcl.p |
|
| Ref | Expression |
|---|---|
| grpcl |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | grpmnd 13591 |
. 2
| |
| 2 | grpcl.b |
. . 3
| |
| 3 | grpcl.p |
. . 3
| |
| 4 | 2, 3 | mndcl 13507 |
. 2
|
| 5 | 1, 4 | syl3an1 1306 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| 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 716 ax-5 1495 ax-7 1496 ax-gen 1497 ax-ie1 1541 ax-ie2 1542 ax-8 1552 ax-10 1553 ax-11 1554 ax-i12 1555 ax-bndl 1557 ax-4 1558 ax-17 1574 ax-i9 1578 ax-ial 1582 ax-i5r 1583 ax-13 2204 ax-14 2205 ax-ext 2213 ax-sep 4207 ax-pow 4264 ax-pr 4299 ax-un 4530 ax-cnex 8123 ax-resscn 8124 ax-1re 8126 ax-addrcl 8129 |
| This theorem depends on definitions: df-bi 117 df-3an 1006 df-tru 1400 df-nf 1509 df-sb 1811 df-eu 2082 df-mo 2083 df-clab 2218 df-cleq 2224 df-clel 2227 df-nfc 2363 df-ral 2515 df-rex 2516 df-rab 2519 df-v 2804 df-sbc 3032 df-un 3204 df-in 3206 df-ss 3213 df-pw 3654 df-sn 3675 df-pr 3676 df-op 3678 df-uni 3894 df-int 3929 df-br 4089 df-opab 4151 df-mpt 4152 df-id 4390 df-xp 4731 df-rel 4732 df-cnv 4733 df-co 4734 df-dm 4735 df-rn 4736 df-res 4737 df-iota 5286 df-fun 5328 df-fn 5329 df-fv 5334 df-ov 6021 df-inn 9144 df-2 9202 df-ndx 13086 df-slot 13087 df-base 13089 df-plusg 13174 df-mgm 13440 df-sgrp 13486 df-mnd 13501 df-grp 13587 |
| This theorem is referenced by: grpcld 13598 grprcan 13621 grprinv 13635 grpressid 13645 grplmulf1o 13658 grpinvadd 13662 grpsubf 13663 grpsubadd 13672 grpaddsubass 13674 grpnpcan 13676 grpsubsub4 13677 grppnpcan2 13678 grplactcnv 13686 imasgrp 13699 mulgcl 13727 mulgaddcomlem 13733 mulgdir 13742 nmzsubg 13798 nsgid 13803 eqgcpbl 13816 qusgrp 13820 qusadd 13822 ecqusaddcl 13827 ghmrn 13845 idghm 13847 ghmnsgima 13856 ghmnsgpreima 13857 ghmf1o 13863 conjghm 13864 qusghm 13870 ablsub4 13901 abladdsub4 13902 invghm 13917 rngacl 13957 rngpropd 13970 ringacl 14045 lmodacl 14315 lmodvacl 14318 rmodislmod 14367 |
| Copyright terms: Public domain | W3C validator |