Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∈ wcel 2107
LModclmod 20365 LVecclvec 20607 PreHilcphl 21051 |
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 ax-nul 5267 |
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-ne 2941 df-ral 3062 df-rab 3407 df-v 3449 df-sbc 3744 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-mpt 5193 df-iota 6452 df-fv 6508 df-ov 7364 df-lvec 20608 df-phl 21053 |
This theorem is referenced by: iporthcom
21062 ip0l
21063 ip0r
21064 ipdir
21066 ipdi
21067 ip2di
21068 ipsubdir
21069 ipsubdi
21070 ip2subdi
21071 ipass
21072 ipassr
21073 ip2eq
21080 phssip
21085 phlssphl
21086 ocvlss
21099 ocvin
21101 ocvlsp
21103 ocvz
21105 ocv1
21106 lsmcss
21119 pjdm2
21140 pjff
21141 pjf2
21143 pjfo
21144 ocvpj
21146 obselocv
21157 obslbs
21159 phclm
24619 ipcau2
24621 tcphcphlem1
24622 tcphcphlem2
24623 tcphcph
24624 pjth
24826 |