We prove:

with no assumptions.

Proof by sequent calculus with unit propagation:

Equivalence goal MouseOver is proven in both directions.

{1} Direction from left to right: Assume:

and prove:

Conjunctive goal MouseOver is decomposed on different proof branches.

{1, 1} Proof of MouseOver:

Implicative goal MouseOver is split. Assume:

and prove:

Implicative assumption MouseOver is used for Modus Ponens.

{1, 1, 1} First the premise of MouseOver is proven:

Disjunctive goal MouseOver is split:

Assumed MouseOver goal MouseOver: success.

{1, 1, 2} Now the conclusion of MouseOver is assumed:

Assumed MouseOver goal MouseOver: success.

{1, 2} Proof of MouseOver:

Implicative goal MouseOver is split. Assume:

and prove:

Implicative assumption MouseOver is used for Modus Ponens.

{1, 2, 1} First the premise of MouseOver is proven:

Disjunctive goal MouseOver is split:

Assumed MouseOver goal MouseOver: success.

{1, 2, 2} Now the conclusion of MouseOver is assumed:

Assumed MouseOver goal MouseOver: success.

{2} Direction from right to left: Assume:

and prove:

Assumed conjunction MouseOver is split into:

Implicative goal MouseOver is split. Assume:

and prove:

Disjunctive assumption MouseOver is used for proof by cases.

{2, 1} Case MouseOver:

Implicative assumption MouseOver is used for Modus Ponens.

{2, 1, 1} First the premise of MouseOver is proven:

Assumed MouseOver goal MouseOver: success.

{2, 1, 2} Now the conclusion of MouseOver is assumed:

Assumed MouseOver goal MouseOver: success.

{2, 2} Case MouseOver:

Implicative assumption MouseOver is used for Modus Ponens.

{2, 2, 1} First the premise of MouseOver is proven:

Implicative assumption MouseOver is used for Modus Ponens.

{2, 2, 1, 1} First the premise of MouseOver is proven:

Assumed MouseOver goal MouseOver: success.

{2, 2, 1, 2} Now the conclusion of MouseOver is assumed:

Assumed MouseOver goal MouseOver: success.

{2, 2, 2} Now the conclusion of MouseOver is assumed:

Assumed MouseOver goal MouseOver: success.