Metamath Proof Explorer


Theorem 2wlkdlem7

Description: Lemma 7 for 2wlkd . (Contributed by AV, 14-Feb-2021)

Ref Expression
Hypotheses 2wlkd.p P = ⟨“ ABC ”⟩
2wlkd.f F = ⟨“ JK ”⟩
2wlkd.s φ A V B V C V
2wlkd.n φ A B B C
2wlkd.e φ A B I J B C I K
Assertion 2wlkdlem7 φ J V K V

Proof

Step Hyp Ref Expression
1 2wlkd.p P = ⟨“ ABC ”⟩
2 2wlkd.f F = ⟨“ JK ”⟩
3 2wlkd.s φ A V B V C V
4 2wlkd.n φ A B B C
5 2wlkd.e φ A B I J B C I K
6 1 2 3 4 5 2wlkdlem6 φ B I J B I K
7 elfvex B I J J V
8 elfvex B I K K V
9 7 8 anim12i B I J B I K J V K V
10 6 9 syl φ J V K V