| 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 13608 |
. 2
| |
| 2 | grpcl.b |
. . 3
| |
| 3 | grpcl.p |
. . 3
| |
| 4 | 2, 3 | mndcl 13524 |
. 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 13103 df-slot 13104 df-base 13106 df-plusg 13191 df-mgm 13457 df-sgrp 13503 df-mnd 13518 df-grp 13604 |
| This theorem is referenced by: grpcld 13615 grprcan 13638 grprinv 13652 grpressid 13662 grplmulf1o 13675 grpinvadd 13679 grpsubf 13680 grpsubadd 13689 grpaddsubass 13691 grpnpcan 13693 grpsubsub4 13694 grppnpcan2 13695 grplactcnv 13703 imasgrp 13716 mulgcl 13744 mulgaddcomlem 13750 mulgdir 13759 nmzsubg 13815 nsgid 13820 eqgcpbl 13833 qusgrp 13837 qusadd 13839 ecqusaddcl 13844 ghmrn 13862 idghm 13864 ghmnsgima 13873 ghmnsgpreima 13874 ghmf1o 13880 conjghm 13881 qusghm 13887 ablsub4 13918 abladdsub4 13919 invghm 13934 rngacl 13974 rngpropd 13987 ringacl 14062 lmodacl 14332 lmodvacl 14335 rmodislmod 14384 |
| Copyright terms: Public domain | W3C validator |