Colors of
variables: wff
setvar class |
Syntax hints:
â wi 4 = wceq 1534
â wcel 2099 Vcvv 3469
âcfv 6542 Vtxcvtx 28796 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906
ax-6 1964 ax-7 2004 ax-8 2101
ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2164 ax-ext 2698 ax-nul 5300 ax-pr 5423 |
This theorem depends on definitions:
df-bi 206 df-an 396
df-or 847 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2529 df-eu 2558 df-clab 2705 df-cleq 2719 df-clel 2805 df-ral 3057 df-rex 3066 df-rab 3428 df-v 3471 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-nul 4319 df-if 4525 df-sn 4625 df-pr 4627 df-op 4631 df-uni 4904 df-br 5143 df-dm 5682 df-iota 6494 df-fv 6550 |
This theorem is referenced by: upgr1e
28913 uspgr1e
29044 nbgrval
29136 cplgr1vlem
29229 vtxdgval
29269 vtxdgelxnn0
29273 wlkson
29457 trlsonfval
29507 pthsonfval
29541 spthson
29542 2wlkd
29734 is0wlk
29914 0wlkon
29917 is0trl
29920 0trlon
29921 0pthon
29924 0clwlkv
29928 1wlkd
29938 3wlkd
29967 wlkl0
30164 |