Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∈ wcel 2099
LModclmod 20732 LVecclvec 20976 PreHilcphl 21543 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906
ax-6 1964 ax-7 2004 ax-8 2101
ax-9 2109 ax-ext 2698 ax-nul 5300 |
This theorem depends on definitions:
df-bi 206 df-an 396
df-or 847 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-sb 2061 df-clab 2705 df-cleq 2719 df-clel 2805 df-ne 2936 df-ral 3057 df-rab 3428 df-v 3471 df-sbc 3775 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-nul 4319 df-if 4525 df-sn 4625 df-pr 4627 df-op 4631 df-uni 4904 df-br 5143 df-opab 5205 df-mpt 5226 df-iota 6494 df-fv 6550 df-ov 7417 df-lvec 20977 df-phl 21545 |
This theorem is referenced by: iporthcom
21554 ip0l
21555 ip0r
21556 ipdir
21558 ipdi
21559 ip2di
21560 ipsubdir
21561 ipsubdi
21562 ip2subdi
21563 ipass
21564 ipassr
21565 ip2eq
21572 phssip
21577 phlssphl
21578 ocvlss
21591 ocvin
21593 ocvlsp
21595 ocvz
21597 ocv1
21598 lsmcss
21611 pjdm2
21632 pjff
21633 pjf2
21635 pjfo
21636 ocvpj
21638 obselocv
21649 obslbs
21651 phclm
25147 ipcau2
25149 tcphcphlem1
25150 tcphcphlem2
25151 tcphcph
25152 pjth
25354 |