Metamath Proof Explorer


Theorem ifpsnprss

Description: Lemma for wlkvtxeledg : Two adjacent (not necessarily different) vertices A and B in a walk are incident with an edge E . (Contributed by AV, 4-Apr-2021) (Revised by AV, 5-Nov-2021)

Ref Expression
Assertion ifpsnprss if- A = B E = A A B E A B E

Proof

Step Hyp Ref Expression
1 ssidd A = B E = A A A
2 preq2 B = A A B = A A
3 dfsn2 A = A A
4 2 3 eqtr4di B = A A B = A
5 4 eqcoms A = B A B = A
6 5 adantr A = B E = A A B = A
7 simpr A = B E = A E = A
8 1 6 7 3sstr4d A = B E = A A B E
9 8 1fpid3 if- A = B E = A A B E A B E