Inference rules for deriving invariants in Hoare logic

Question

The following algorithm is supposed to compare two strings $S_1$ and $S_2$ ("/\" for empty string):

X = S1   
Y = S2

E = true   
// (1) S1 = S2 <=> X = Y and E = true
while X != /\ and Y != /\ and E == true          
  if head(X) == head(Y)           
    X = tail(X)
    Y = tail(Y)
  else
    E = false
// (2) S1 = S2 <=> X = /\ and Y = /\ and E = true
if !(X == /\ and Y == /\)    
  E = false 
  // (3) S1 != S2 and E = false
else // an empty else; just for inserting an assertion (i.e., 3' below) here
  // (3') S1 = S2 <=> E = true
// (4) S1 = S2 <=> E = true
return E

There are five invariants:

(1). $S_1 = S_2 \iff X = Y \land E = true$

(2). $S_1 = S_2 \iff X = \Lambda \land Y = \Lambda \land E = true$

(3). $S_1 \neq S_2 \land E = false$

(3'). $S_1 = S_2 \iff E = true$

(4). $S_1 = S_2 \iff E = true$

I can understand these invariants and how they are derived from the previous ones in an intuitive and thus informal way. For example, we can derive (3') from (2) as follows:

At point (2), we know that $S_1$ equals $S_2$ iff $X = \Lambda \land Y = \Lambda \land E = true$. At point (3'), we further know that $X = \Lambda \land Y = \Lambda$. Thus, at this point, we only need to check whether $E = true$ to decide whether $S_1 = S_2$ holds.

However, the reasoning above cannot be justified by the conventional inference rules of propositional logic by which we would have

$$S_1 = S_2 \iff (X = \Lambda \land Y = \Lambda \land E = true) \land (X = \Lambda \land Y = \Lambda),$$ which is $S_1 = S_2 \iff X = \Lambda \land Y = \Lambda \land E = true.$

---

Problem: What are the inference rules for the derivation from (2) to (3')?

Related Post: Developing invariants for comparing two strings

---

Edit: As pointed out by @chi in the comment, it should be $$\big(S_1 = S_2 \iff (X = \Lambda \land Y = \Lambda \land E = true)\big) \land (X = \Lambda \land Y = \Lambda),$$ which implies (3') $S_1 = S_2 \iff E = true$ as the answer given by @kne shows.