Colors of
variables: wff
setvar class |
Syntax hints:
β wi 4 β wcel 2107
β wss 3914 β
ccom 5641 βcfv 6500
distcds 17150 Grpcgrp 18756
-gcsg 18758
MetSpcms 23694 normcnm 23955
NrmGrpcngp 23956 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914
ax-6 1972 ax-7 2012 ax-8 2109
ax-9 2117 ax-ext 2704 |
This theorem depends on definitions:
df-bi 206 df-an 398
df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-rab 3407 df-v 3449 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-nul 4287 df-if 4491 df-sn 4591 df-pr 4593 df-op 4597 df-uni 4870 df-br 5110 df-opab 5172 df-co 5646 df-iota 6452 df-fv 6508 df-ngp 23962 |
This theorem is referenced by: ngpds
23983 ngpds2
23985 ngpds3
23987 ngprcan
23989 isngp4
23991 ngpinvds
23992 ngpsubcan
23993 nmf
23994 nmge0
23996 nmeq0
23997 nminv
24000 nmmtri
24001 nmsub
24002 nmrtri
24003 nm2dif
24004 nmtri
24005 nmtri2
24006 ngpi
24007 nm0
24008 ngptgp
24015 tngngp2
24039 tnggrpr
24042 nrmtngnrm
24045 nlmdsdi
24068 nlmdsdir
24069 nrginvrcnlem
24078 ngpocelbl
24091 nmo0
24122 nmotri
24126 0nghm
24128 nmoid
24129 idnghm
24130 nmods
24131 nmcn
24230 nmoleub2lem2
24502 nmhmcn
24506 cphpyth
24603 cphipval2
24628 4cphipval2
24629 cphipval
24630 ipcnlem2
24631 nglmle
24689 qqhcn
32636 |