Step | Hyp | Ref
| Expression |
1 | | simp3l 1089 |
. . . 4
FriendGraph
|
2 | | eqid 2622 |
. . . . 5
Vtx Vtx |
3 | 2 | wwlks2onv 26847 |
. . . 4
WWalksNOn Vtx
Vtx Vtx |
4 | 1, 3 | sylan 488 |
. . 3
FriendGraph WWalksNOn Vtx
Vtx Vtx |
5 | | simp3r 1090 |
. . . . . . . 8
FriendGraph
|
6 | 2 | wwlks2onv 26847 |
. . . . . . . 8
WWalksNOn Vtx
Vtx Vtx |
7 | 5, 6 | sylan 488 |
. . . . . . 7
FriendGraph WWalksNOn Vtx
Vtx Vtx |
8 | | frgrusgr 27124 |
. . . . . . . . . . . . . . 15
FriendGraph USGraph |
9 | | usgrumgr 26074 |
. . . . . . . . . . . . . . 15
USGraph UMGraph |
10 | 8, 9 | syl 17 |
. . . . . . . . . . . . . 14
FriendGraph UMGraph |
11 | 10 | 3ad2ant1 1082 |
. . . . . . . . . . . . 13
FriendGraph
UMGraph |
12 | | simpr3 1069 |
. . . . . . . . . . . . . 14
Vtx
Vtx
Vtx
Vtx
Vtx |
13 | | simpl 473 |
. . . . . . . . . . . . . 14
Vtx
Vtx
Vtx
Vtx
Vtx |
14 | | simpr1 1067 |
. . . . . . . . . . . . . 14
Vtx
Vtx
Vtx
Vtx
Vtx |
15 | 12, 13, 14 | 3jca 1242 |
. . . . . . . . . . . . 13
Vtx
Vtx
Vtx
Vtx Vtx
Vtx
Vtx |
16 | 2 | wwlks2onsym 26851 |
. . . . . . . . . . . . 13
UMGraph
Vtx
Vtx
Vtx WWalksNOn
WWalksNOn |
17 | 11, 15, 16 | syl2anr 495 |
. . . . . . . . . . . 12
Vtx
Vtx Vtx
Vtx FriendGraph
WWalksNOn
WWalksNOn |
18 | | simpr1 1067 |
. . . . . . . . . . . . . 14
Vtx
Vtx Vtx
Vtx FriendGraph
FriendGraph |
19 | | 3simpb 1059 |
. . . . . . . . . . . . . . 15
Vtx Vtx
Vtx Vtx
Vtx |
20 | 19 | ad2antlr 763 |
. . . . . . . . . . . . . 14
Vtx
Vtx Vtx
Vtx FriendGraph
Vtx
Vtx |
21 | | simpr2 1068 |
. . . . . . . . . . . . . 14
Vtx
Vtx Vtx
Vtx FriendGraph
|
22 | 2 | frgr2wwlkeu 27191 |
. . . . . . . . . . . . . 14
FriendGraph Vtx
Vtx
Vtx WWalksNOn |
23 | 18, 20, 21, 22 | syl3anc 1326 |
. . . . . . . . . . . . 13
Vtx
Vtx Vtx
Vtx FriendGraph
Vtx WWalksNOn |
24 | | s3eq2 13615 |
. . . . . . . . . . . . . . . . 17
|
25 | 24 | eleq1d 2686 |
. . . . . . . . . . . . . . . 16
WWalksNOn
WWalksNOn |
26 | 25 | riota2 6633 |
. . . . . . . . . . . . . . 15
Vtx
Vtx WWalksNOn WWalksNOn
Vtx WWalksNOn |
27 | 26 | ad4ant14 1293 |
. . . . . . . . . . . . . 14
Vtx Vtx
Vtx
Vtx FriendGraph
Vtx WWalksNOn WWalksNOn
Vtx WWalksNOn |
28 | | simplr2 1104 |
. . . . . . . . . . . . . . . . 17
Vtx
Vtx Vtx
Vtx FriendGraph
Vtx |
29 | | s3eq2 13615 |
. . . . . . . . . . . . . . . . . . 19
|
30 | 29 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . 18
WWalksNOn
WWalksNOn |
31 | 30 | riota2 6633 |
. . . . . . . . . . . . . . . . 17
Vtx
Vtx WWalksNOn WWalksNOn
Vtx WWalksNOn |
32 | 28, 31 | sylan 488 |
. . . . . . . . . . . . . . . 16
Vtx Vtx
Vtx
Vtx FriendGraph
Vtx WWalksNOn WWalksNOn
Vtx WWalksNOn |
33 | | eqtr2 2642 |
. . . . . . . . . . . . . . . . 17
Vtx WWalksNOn Vtx WWalksNOn
|
34 | 33 | expcom 451 |
. . . . . . . . . . . . . . . 16
Vtx WWalksNOn Vtx WWalksNOn |
35 | 32, 34 | syl6bi 243 |
. . . . . . . . . . . . . . 15
Vtx Vtx
Vtx
Vtx FriendGraph
Vtx WWalksNOn WWalksNOn Vtx WWalksNOn |
36 | 35 | com23 86 |
. . . . . . . . . . . . . 14
Vtx Vtx
Vtx
Vtx FriendGraph
Vtx WWalksNOn Vtx WWalksNOn WWalksNOn
|
37 | 27, 36 | sylbid 230 |
. . . . . . . . . . . . 13
Vtx Vtx
Vtx
Vtx FriendGraph
Vtx WWalksNOn WWalksNOn WWalksNOn
|
38 | 23, 37 | mpdan 702 |
. . . . . . . . . . . 12
Vtx
Vtx Vtx
Vtx FriendGraph
WWalksNOn WWalksNOn
|
39 | 17, 38 | sylbid 230 |
. . . . . . . . . . 11
Vtx
Vtx Vtx
Vtx FriendGraph
WWalksNOn WWalksNOn
|
40 | 39 | expimpd 629 |
. . . . . . . . . 10
Vtx
Vtx
Vtx
Vtx FriendGraph
WWalksNOn
WWalksNOn |
41 | 40 | ex 450 |
. . . . . . . . 9
Vtx
Vtx
Vtx
Vtx FriendGraph
WWalksNOn
WWalksNOn |
42 | 41 | com23 86 |
. . . . . . . 8
Vtx
FriendGraph WWalksNOn Vtx
Vtx
Vtx WWalksNOn
|
43 | 42 | 3ad2ant2 1083 |
. . . . . . 7
Vtx Vtx
Vtx FriendGraph
WWalksNOn
Vtx
Vtx
Vtx WWalksNOn
|
44 | 7, 43 | mpcom 38 |
. . . . . 6
FriendGraph WWalksNOn Vtx
Vtx
Vtx WWalksNOn
|
45 | 44 | ex 450 |
. . . . 5
FriendGraph
WWalksNOn Vtx
Vtx Vtx
WWalksNOn |
46 | 45 | com24 95 |
. . . 4
FriendGraph
WWalksNOn Vtx
Vtx Vtx
WWalksNOn |
47 | 46 | imp 445 |
. . 3
FriendGraph WWalksNOn Vtx
Vtx
Vtx WWalksNOn
|
48 | 4, 47 | mpd 15 |
. 2
FriendGraph WWalksNOn WWalksNOn
|
49 | 48 | expimpd 629 |
1
FriendGraph
WWalksNOn WWalksNOn |