Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∈ wcel 2106
LModclmod 20470 LVecclvec 20712 PreHilcphl 21176 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913
ax-6 1971 ax-7 2011 ax-8 2108
ax-9 2116 ax-ext 2703 ax-nul 5306 |
This theorem depends on definitions:
df-bi 206 df-an 397
df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-sb 2068 df-clab 2710 df-cleq 2724 df-clel 2810 df-ne 2941 df-ral 3062 df-rab 3433 df-v 3476 df-sbc 3778 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-br 5149 df-opab 5211 df-mpt 5232 df-iota 6495 df-fv 6551 df-ov 7411 df-lvec 20713 df-phl 21178 |
This theorem is referenced by: iporthcom
21187 ip0l
21188 ip0r
21189 ipdir
21191 ipdi
21192 ip2di
21193 ipsubdir
21194 ipsubdi
21195 ip2subdi
21196 ipass
21197 ipassr
21198 ip2eq
21205 phssip
21210 phlssphl
21211 ocvlss
21224 ocvin
21226 ocvlsp
21228 ocvz
21230 ocv1
21231 lsmcss
21244 pjdm2
21265 pjff
21266 pjf2
21268 pjfo
21269 ocvpj
21271 obselocv
21282 obslbs
21284 phclm
24748 ipcau2
24750 tcphcphlem1
24751 tcphcphlem2
24752 tcphcph
24753 pjth
24955 |