Need help to check/extend a proof.

Another question from the archive:

L = {<M1><M2><M3>|L(M1)!=L(M2) and L(M2)!=L(M3) and L(M1)!=L(M3)}
Is this recursive? RE but not recursive? Not RE?

<Mi> is the encoding of TM Mi.

I started my proof with a 2 machine case:

We know that
1. L2 = {<M1><M2>|L(M1)=L(M2)} is undecidable
2. L2' = {<M1><M2>|L(M1)!=L(M2)} is the complement of L2

So we know that L2' is not recursive. I try to proof that L2' is RE:

To prove L(M1)!=L(M2), we only need one string that L(M1) accepts and
L(M2) does not.

So we construct a non-deterministic TM M-sim that simulates M1 and M2
in parallel. The input to M-sim is <M1><M2>. The simulated M1 and M2
uses a "guessed" (non-deterministic) string w as input. M-sim only
accepts if for some w, M1 or M2 goes to the accepting state but not
both.

Thus L(M-sim) = L2', and L2' is RE.

Is this proof correct?

If so, is it trivial to extend it to the three-machine case?

Thanks for any reply.

.