Inference rules for deriving invariants in Hoare logic
There are two ways to answer the question.

The first is on the level of propositional logic. You have three statements, $S_1=S_2$, $(X=\Lambda\wedge Y=\Lambda)$, and $E=true$. Let's call them $A$, $B$, and $C$ for short. (2) is $A\Leftrightarrow(B\wedge C)$ and (3') is $A\Leftrightarrow C$. At point (3') we know $B$. Every assignment of the propositional variables that satisfies $B$ and (2) also satisfies (3'). In other words, at the position (3') we know

$(A\Leftrightarrow(B\wedge C))\wedge B$

from which

$(A\Leftrightarrow C)$

follows semantically. If the propositional proof system of your choice is complete, the above can also be derived using its rules.

The second answer addresses Hoare logic instead of propositional logic. Hoare logic has its own derivations. The neat thing is that most of them can be automated. And they work backwards. In the case at hand, (3') is derived from (4) by copy. After all, at the end of the else clause, the same invariant must hold as after the if-then-else. The then clause does not follow that rule, so let us fix the code

// (2) S1 = S2 &lt;=&gt; X = /\ and Y = /\ and E = true
// (2') (!(X == /\ and Y == /\) and (S1 = S2 &lt;=&gt; false = true)) or
//    ((X == /\ and Y == /\) and (S1 = S2 &lt;=&gt; E = true))
if !(X == /\ and Y == /\)    
  // (3'') S1 = S2 &lt;=&gt; false = true
  E = false 
  // (3) S1 = S2 &lt;=&gt; E = true
else // an empty else
  // (3') S1 = S2 &lt;=&gt; E = true
// (4) S1 = S2 &lt;=&gt; E = true


Now (3) is derived from (4) by copy, (3'') is derived from (3) by substitution (that is the Hoare logic rule for assignment) and (2') is derived from (3''), (3') and the if condition. It remains to see how (2') follows from (2). That is propositional logic plus $false\not=true$.