Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  usgra2wlkspth Unicode version

Theorem usgra2wlkspth 28666
Description: In a undirected simple graph, any walk of length 2 between two different vertices is a simple path. (Contributed by Alexander van der Vekens, 2-Mar-2018.)
Assertion
Ref Expression
usgra2wlkspth

Proof of Theorem usgra2wlkspth
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 wlkonprop 21568 . . . 4
2 simplr 733 . . . . . 6
3 iswlk 21563 . . . . . . . . . . . . . . . 16
433adant3 978 . . . . . . . . . . . . . . 15
5 id 21 . . . . . . . . . . . . . . . . . . . . 21
653ad2ant1 979 . . . . . . . . . . . . . . . . . . . 20
76ad4antlr 715 . . . . . . . . . . . . . . . . . . 19
8 usgraf1 21419 . . . . . . . . . . . . . . . . . . . . . . 23
983ad2ant1 979 . . . . . . . . . . . . . . . . . . . . . 22
109adantl 454 . . . . . . . . . . . . . . . . . . . . 21
11 simp2 959 . . . . . . . . . . . . . . . . . . . . . 22
1211adantl 454 . . . . . . . . . . . . . . . . . . . . 21
137, 10, 123jca 1135 . . . . . . . . . . . . . . . . . . . 20
14 simpl 445 . . . . . . . . . . . . . . . . . . . . . . 23
1514ad3antlr 713 . . . . . . . . . . . . . . . . . . . . . 22
16 simpr 449 . . . . . . . . . . . . . . . . . . . . . . 23
1716ad3antlr 713 . . . . . . . . . . . . . . . . . . . . . 22
18 simp3 960 . . . . . . . . . . . . . . . . . . . . . . 23
1918adantl 454 . . . . . . . . . . . . . . . . . . . . . 22
2015, 17, 193jca 1135 . . . . . . . . . . . . . . . . . . . . 21
21 simp3 960 . . . . . . . . . . . . . . . . . . . . . 22
2221ad4antlr 715 . . . . . . . . . . . . . . . . . . . . 21
2320, 22jca 520 . . . . . . . . . . . . . . . . . . . 20
24 usgra2wlkspthlem1 28664 . . . . . . . . . . . . . . . . . . . 20
2513, 23, 24sylc 59 . . . . . . . . . . . . . . . . . . 19
267, 25jca 520 . . . . . . . . . . . . . . . . . 18
27 simp2 959 . . . . . . . . . . . . . . . . . . 19
2827ad4antlr 715 . . . . . . . . . . . . . . . . . 18
2926, 28, 223jca 1135 . . . . . . . . . . . . . . . . 17
3029exp31 589 . . . . . . . . . . . . . . . 16
3130exp31 589 . . . . . . . . . . . . . . 15
324, 31sylbid 208 . . . . . . . . . . . . . 14
3332com13 77 . . . . . . . . . . . . 13
3433ex 425 . . . . . . . . . . . 12
3534com3r 76 . . . . . . . . . . 11
36353imp 1148 . . . . . . . . . 10
3736impcom 421 . . . . . . . . 9
3837imp31 423 . . . . . . . 8
39 id 21 . . . . . . . . . . 11
40393adant3 978 . . . . . . . . . 10
4140ad3antrrr 712 . . . . . . . . 9
42 istrl 21573 . . . . . . . . 9
4341, 42syl 16 . . . . . . . 8
4438, 43mpbird 225 . . . . . . 7
45 2mwlk 21564 . . . . . . . . . . . . 13
46 simpl 445 . . . . . . . . . . . . 13
4745, 46syl 16 . . . . . . . . . . . 12
48473ad2ant1 979 . . . . . . . . . . 11
4948ad3antlr 713 . . . . . . . . . 10
5011adantl 454 . . . . . . . . . 10
5149, 50jca 520 . . . . . . . . 9
52 id 21 . . . . . . . . . . . 12
53523ad2ant1 979 . . . . . . . . . . 11
5453adantl 454 . . . . . . . . . 10
55 simpr 449 . . . . . . . . . . . . 13
5645, 55syl 16 . . . . . . . . . . . 12
57563ad2ant1 979 . . . . . . . . . . 11
5857ad3antlr 713 . . . . . . . . . 10
5954, 58jca 520 . . . . . . . . 9
6051, 59jca 520 . . . . . . . 8
61 simp2 959 . . . . . . . . . . 11
6261ad3antlr 713 . . . . . . . . . 10
63 simp3 960 . . . . . . . . . . 11
6463ad3antlr 713 . . . . . . . . . 10
6518adantl 454 . . . . . . . . . 10
6662, 64, 653jca 1135 . . . . . . . . 9
674, 21syl6bi 221 . . . . . . . . . . . . 13
6867com12 30 . . . . . . . . . . . 12
69683ad2ant1 979 . . . . . . . . . . 11
7069impcom 421 . . . . . . . . . 10
7170ad2antrr 708 . . . . . . . . 9
7266, 71jca 520 . . . . . . . 8
73 usgra2wlkspthlem2 28665 . . . . . . . 8
7460, 72, 73sylc 59 . . . . . . 7
75 isspth 21605 . . . . . . . 8