Metamath Proof Explorer


Theorem 1wlkdlem2

Description: Lemma 2 for 1wlkd . (Contributed by AV, 22-Jan-2021)

Ref Expression
Hypotheses 1wlkd.p P = ⟨“ XY ”⟩
1wlkd.f F = ⟨“ J ”⟩
1wlkd.x φ X V
1wlkd.y φ Y V
1wlkd.l φ X = Y I J = X
1wlkd.j φ X Y X Y I J
Assertion 1wlkdlem2 φ X I J

Proof

Step Hyp Ref Expression
1 1wlkd.p P = ⟨“ XY ”⟩
2 1wlkd.f F = ⟨“ J ”⟩
3 1wlkd.x φ X V
4 1wlkd.y φ Y V
5 1wlkd.l φ X = Y I J = X
6 1wlkd.j φ X Y X Y I J
7 snidg X V X X
8 3 7 syl φ X X
9 8 adantr φ X = Y X X
10 9 5 eleqtrrd φ X = Y X I J
11 4 adantr φ X Y Y V
12 prssg X V Y V X I J Y I J X Y I J
13 3 11 12 syl2an2r φ X Y X I J Y I J X Y I J
14 6 13 mpbird φ X Y X I J Y I J
15 14 simpld φ X Y X I J
16 10 15 pm2.61dane φ X I J