Colors of
variables: wff
setvar class |
Syntax hints: ¬ wn 3 → wi 4
Ⅎwnf 1786 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1798 ax-4 1812 |
This theorem depends on definitions:
df-bi 206 df-or 847
df-ex 1783 df-nf 1787 |
This theorem is referenced by: nfand
1901 nfan1
2194 hbnt
2291 nfexd
2323 cbvexdw
2336 cbvexd
2407 nfexd2
2445 nfned
3047 nfneld
3058 nfrexdw
3296 nfrexd
3349 vtoclgft
3512 axpowndlem3
10542 axpowndlem4
10543 axregndlem2
10546 axregnd
10547 distel
34417 bj-cbvexdv
35294 bj-nfexd
35638 wl-issetft
36063 |