Colors of
variables: wff
setvar class |
Syntax hints:
= wceq 1541 ↾ cres 5678 |
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 |
This theorem depends on definitions:
df-bi 206 df-an 397
df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2710 df-cleq 2724 df-clel 2810 df-rab 3433 df-in 3955 df-opab 5211 df-xp 5682 df-res 5688 |
This theorem is referenced by: cnvresid
6627 fprlem1
8287 wfrlem5OLD
8315 dfoi
9508 frrlem15
9754 lubfval
18305 glbfval
18318 odulub
18362 oduglb
18364 dvlog
26166 dvlog2
26168 issubgr
28566 finsumvtxdg2size
28845 sitgclg
33410 fourierdlem57
44958 fourierdlem74
44975 fourierdlem75
44976 |