Metamath Proof Explorer


Theorem 2wlkdlem3

Description: Lemma 3 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
Assertion 2wlkdlem3 φ P 0 = A P 1 = B P 2 = C

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 1 fveq1i P 0 = ⟨“ ABC ”⟩ 0
5 s3fv0 A V ⟨“ ABC ”⟩ 0 = A
6 4 5 syl5eq A V P 0 = A
7 1 fveq1i P 1 = ⟨“ ABC ”⟩ 1
8 s3fv1 B V ⟨“ ABC ”⟩ 1 = B
9 7 8 syl5eq B V P 1 = B
10 1 fveq1i P 2 = ⟨“ ABC ”⟩ 2
11 s3fv2 C V ⟨“ ABC ”⟩ 2 = C
12 10 11 syl5eq C V P 2 = C
13 6 9 12 3anim123i A V B V C V P 0 = A P 1 = B P 2 = C
14 3 13 syl φ P 0 = A P 1 = B P 2 = C