Colors of
variables: wff
setvar class |
Syntax hints: -> wi 4 <-> wb 184
A. wal 1393 F/ wnf 1616 |
This theorem is referenced by: nfbidf
1887 dral2
2066 dral1
2067 ax12v2
2083 sbal1
2204 sbal2
2205 ax12eq
2271 ax12el
2272 ax12v2-o
2279 eubid
2302 ralbida
2890 raleqf
3050 intab
4317 fin23lem32
8745 axrepndlem1
8988 axrepndlem2
8989 axrepnd
8990 axunnd
8992 axpowndlem2
8994 axpowndlem2OLD
8995 axpowndlem4
8998 axregndlem2
9001 axinfndlem1
9004 axinfnd
9005 axacndlem4
9009 axacndlem5
9010 axacnd
9011 funcnvmptOLD
27509 iota5f
29102 wl-equsald
29992 wl-sbnf1
30003 wl-2sb6d
30008 wl-sbalnae
30012 wl-mo2dnae
30019 wl-ax11-lem6
30030 wl-ax11-lem8
30032 bj-dral1v
34326 bj-axc15v
34330 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1618 ax-4 1631 ax-5 1704
ax-6 1747 ax-7 1790 ax-12 1854 |
This theorem depends on definitions:
df-bi 185 df-ex 1613 df-nf 1617 |