Colors of
variables: wff set class |
Syntax hints:
→ wi 4 ∀wal 1351
Ⅎwnf 1460 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-ia1 106 ax-5 1447 ax-gen 1449 ax-4 1510 |
This theorem depends on definitions:
df-bi 117 df-nf 1461 |
This theorem is referenced by: axc4i
1542 19.32r
1680 cbv3
1742 sbbid
1846 sbalyz
1999 dvelimdf
2016 dvelimor
2018 nf5d
2025 abbid
2294 nfcd
2314 nfabdw
2338 ralrimi
2548 r19.32r
2623 ceqsalg
2767 ceqsex
2777 vtocldf
2790 elrab3t
2894 morex
2923 sbciedf
3000 csbiebt
3098 csbiedf
3099 ssrd
3162 rgenm
3527 invdisj
3999 ssopab2b
4278 eusv2nf
4458 sniota
5209 imadif
5298 funimaexglem
5301 eusvobj1
5864 ssoprab2b
5934 ovmpodxf
6002 |