Proving XOR Commutativity: Sufficiency of Tautology

[gnome]

Given that XOR is defined by ((X \wedge \neg Y) \vee (\neg X \wedge Y)), in order to prove that XOR is commutative is it sufficient to prove that
((X \wedge \neg Y) \vee (\neg X \wedge Y)) \supset ((Y \wedge \neg X) \vee (\neg Y \wedge X))
is a tautology?

 

[Hurkyl]

Think about what that says:

If (X xor Y), then (Y xor X).

Is that the same as X xor Y = Y xor X?

(no)

Now, in general you would leave the last step implicit, because it's fairly routine, but I imagine you're interested in full rigor.

 

[gnome]

OK, I'd like to retract that ridiculous statement before I get banned.

Maybe I'd better get some sleep... :zzz: