Metamath Proof Explorer

Theorem umgr2adedgwlklem

Description: Lemma for umgr2adedgwlk , umgr2adedgspth , etc. (Contributed by Alexander van der Vekens, 1-Feb-2018) (Revised by AV, 29-Jan-2021)

Ref Expression
Hypothesis umgr2adedgwlk.e ⊢E=Edg⁡G
Assertion umgr2adedgwlklem ⊢G∈UMGraph∧AB∈E∧BC∈E→A≠B∧B≠C∧A∈Vtx⁡G∧B∈Vtx⁡G∧C∈Vtx⁡G

Proof

Step Hyp Ref Expression
1 umgr2adedgwlk.e ⊢E=Edg⁡G
2 1 umgredgne ⊢G∈UMGraph∧AB∈E→A≠B
3 2 ex ⊢G∈UMGraph→AB∈E→A≠B
4 1 umgredgne ⊢G∈UMGraph∧BC∈E→B≠C
5 4 ex ⊢G∈UMGraph→BC∈E→B≠C
6 3 5 anim12d ⊢G∈UMGraph→AB∈E∧BC∈E→A≠B∧B≠C
7 6 3impib ⊢G∈UMGraph∧AB∈E∧BC∈E→A≠B∧B≠C
8 eqid ⊢Vtx⁡G=Vtx⁡G
9 8 1 umgrpredgv ⊢G∈UMGraph∧AB∈E→A∈Vtx⁡G∧B∈Vtx⁡G
10 9 simpld ⊢G∈UMGraph∧AB∈E→A∈Vtx⁡G
11 10 3adant3 ⊢G∈UMGraph∧AB∈E∧BC∈E→A∈Vtx⁡G
12 8 1 umgrpredgv ⊢G∈UMGraph∧BC∈E→B∈Vtx⁡G∧C∈Vtx⁡G
13 12 simpld ⊢G∈UMGraph∧BC∈E→B∈Vtx⁡G
14 13 3adant2 ⊢G∈UMGraph∧AB∈E∧BC∈E→B∈Vtx⁡G
15 12 simprd ⊢G∈UMGraph∧BC∈E→C∈Vtx⁡G
16 15 3adant2 ⊢G∈UMGraph∧AB∈E∧BC∈E→C∈Vtx⁡G
17 11 14 16 3jca ⊢G∈UMGraph∧AB∈E∧BC∈E→A∈Vtx⁡G∧B∈Vtx⁡G∧C∈Vtx⁡G
18 7 17 jca ⊢G∈UMGraph∧AB∈E∧BC∈E→A≠B∧B≠C∧A∈Vtx⁡G∧B∈Vtx⁡G∧C∈Vtx⁡G