Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∀wal 1540 |
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-10 2138 ax-12 2172 |
This theorem depends on definitions:
df-bi 206 df-or 847
df-ex 1783 df-nf 1787 |
This theorem is referenced by: hbae
2431 hbsb2
2482 hbsb2a
2484 hbsb2e
2486 nfabdwOLD
2928 reu6
3723 ralidm
4512 axunndlem1
10590 axacndlem3
10604 axacndlem5
10606 axacnd
10607 bj-nfs1t
35668 bj-hbs1
35690 bj-hbsb2av
35692 bj-hbaeb2
35696 wl-hbae1
36388 frege93
42707 spALT
42953 pm11.57
43148 pm11.59
43150 axc5c4c711toc7
43163 axc11next
43165 hbalg
43316 ax6e2eq
43318 ax6e2eqVD
43668 ichnfimlem
46131 |