Colors of
variables: wff set class |
Syntax hints:
→ wi 4 = wceq 1364
‘cfv 5231 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 710
ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-ext 2171 |
This theorem depends on definitions:
df-bi 117 df-3an 982 df-tru 1367 df-nf 1472 df-sb 1774 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-rex 2474 df-v 2754 df-un 3148 df-sn 3613 df-pr 3614 df-op 3616 df-uni 3825 df-br 4019 df-iota 5193 df-fv 5239 |
This theorem is referenced by: nffvd
5542 fvsng
5728 tfrlem3ag
6328 tfrlem3a
6329 tfrlemi1
6351 tfr1onlem3ag
6356 omp1eomlem
7111 seq3shft
10865 climshft2
11332 fsum3
11413 ctiunctlemfo
12458 imasival
12749 mulgfvalg
13029 mulgval
13030 mulgnndir
13057 mulgpropdg
13070 unitinvinv
13435 rlmvalg
13731 rsp0
13770 znval
13893 reldvg
14545 dvfvalap
14547 lgsval
14802 lgsneg
14822 |