Colors of
variables: wff
setvar class |
Syntax hints:
β wi 4 β wcel 2104
βcfv 6458 AbsValcabv 20121 normcnm 23777
NrmGrpcngp 23778 NrmRingcnrg 23780 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911
ax-6 1969 ax-7 2009 ax-8 2106
ax-9 2114 ax-ext 2707 |
This theorem depends on definitions:
df-bi 206 df-an 398
df-or 846 df-3an 1089 df-tru 1542 df-fal 1552 df-ex 1780 df-sb 2066 df-clab 2714 df-cleq 2728 df-clel 2814 df-rab 3287 df-v 3439 df-dif 3895 df-un 3897 df-in 3899 df-ss 3909 df-nul 4263 df-if 4466 df-sn 4566 df-pr 4568 df-op 4572 df-uni 4845 df-br 5082 df-iota 6410 df-fv 6466 df-nrg 23786 |
This theorem is referenced by: nrgdsdi
23874 nrgdsdir
23875 unitnmn0
23877 nminvr
23878 nmdvr
23879 nrgtgp
23881 subrgnrg
23882 nlmngp2
23889 sranlm
23893 nrginvrcnlem
23900 nrginvrcn
23901 cnzh
31965 rezh
31966 qqhcn
31986 qqhucn
31987 rrhcn
31992 rrhf
31993 rrexttps
32001 rrexthaus
32002 |