All such problems are trivial when expressed in a suitable formal system for propositional calculus.

For example, you might try expressing your problem in logical graphs — see here or here and here — then checking the required equation by using the four axioms of that system.

## Addenda

*The lack of LaTeX in the comment boxes is a major headache, so I'll add my comments and elaborations here.*

**Comment 1**

I'm guessing that you're using "+" for inclusive disjunction "$\lor$". This has turned out to be a bad practice, leading to major breaches of communication among mathematicians, computer scientists, and engineers. It is best to save "+" for the field operation, in this case corresponding to the operation of exclusive disjunction and the relation of logical inequality. Besides, we already have the symbol "$\lor$", so we might as vel use it.

**Comment 2**

Proceeding on the maxim, "Act Locally, Think Globally", let us take this very simple example as a paradigmatic case and use it to explore several themes involving the variety of formal systems that afford interpretation as propositional calculi.

One theme worth developing has to do with the choice among various "proof styles". Two dimensions of proof style that come to mind are these:

- Equational Proofs
*vs.* Implicational Proofs
- Insight Proofs
*vs.* Routine Proofs

**Equational Proofs** are those that use only 2-way inference rules. There is no loss of information in applying an equational rule of inference, and so the corresponding syntactic transformation is fully reversible.

**Implicational Proofs** are those that use 1-way inference rules like *modus ponens*. There is in general a loss of information in applying an implicational rule of inference.

**Insight Proofs** are those that require a modicum of cleverness or strategy on the part of the prover.

**Routine Proofs** are those that can be applied in a lock-step form of procedure or a straightforwardly methodical manner, suitable for automation by a mechanical prover.

**Comment 3**

The required equation between two expressions of the 3-majority function $f : \mathbb{B}^3 \to \mathbb{B}$ is proven below by means of equational inference steps in the syntax of logical graphs. I don't know if this is the best possible proof — it's simply the one that came to me first. The only bit of cleverness or "insight" required comes at the very beginning, where a step of "Reflection" or Double Negation is needed to prepare the ground. Everything after that is pretty much like rolling off a log. The axioms, theorems, and familiar names for the inference rules are given in this PlanetMath entry, also here if that doesn't work.

Here's an animated recap of the graphical transformations that occur in the above proof:

Further explanation of Proof 1 can be found here.