I need to prove the following is a theorem in $\mathbf{S5}$:
$$ \Diamond A \wedge \Diamond B \rightarrow (\Diamond (A \wedge \Diamond B) \vee \Diamond (B \wedge \Diamond A)). $$
I have the following axioms: (i) $\Box A \rightarrow A$
(ii) $\Box A \rightarrow \Box \Box A$
(iii) $A \rightarrow \Box \Diamond A$
and the duals of these, and the standard axioms, theorems and rules of minimal modal logic.
I know there is also a theorem of S5, namely (iv) $\Diamond A \rightarrow \Box \Diamond A$.
Attempt: I had so far: 1) $A \wedge B \rightarrow A \wedge \Diamond B$ by dual of (i).
Similarly 2) $A \wedge B \rightarrow \Diamond A \wedge B$
Hence 3) $A \wedge B \rightarrow (A \wedge \Diamond B) \vee ( \Diamond A \wedge B)$.
Then 4) $$ \Diamond \Diamond \Box (A \wedge B) \rightarrow \Diamond \Diamond \Box [ (A \wedge \Diamond B) \vee ( \Diamond A \wedge B)]$$ from 3) applying Becker rule.
But 5) $$ \Diamond \Diamond \Box [ (A \wedge \Diamond B) \vee ( \Diamond A \wedge B)] \rightarrow \Diamond [(A \wedge \Diamond B) \vee ( \Diamond A \wedge B)] $$ by dual of (iii).
Since $\Diamond \phi \vee \Diamond \psi \leftrightarrow \Diamond (\phi \vee \psi)$ is a standard rule, the consequence of 5) would imply the desired result. So it is sufficient to prove that $$ \Diamond A \wedge \Diamond B \rightarrow \Diamond \Diamond \Box (A \wedge B). $$ And this is the part where I am stuck.
Anyone has advice? Thank you in advance.
There is a good reason why you cannot prove the part where you're stuck: it is not anywhere close to valid. It is a good idea to learn semantics, even if you are required to work with formal systems, so you can easily recognize these things.
Something crucial about S5 is that once you put a modal operator on something, additional modal operators don't do anything. It's very quick to prove just from the axioms you wrote down that $\square\square A\leftrightarrow \square A$ and $\square\lozenge A\leftrightarrow\lozenge A.$
I'm not sure what the assigner of this exercise had in mind, but this theorem is way weaker than it needs to be. In fact, the premise is equivalent to both of the disjuncts in the conclusion (another thing semantics will allow you to see easily). So we can just prove $(\lozenge A\land\lozenge B)\to \lozenge(A\land \lozenge B),$ or in dual form, $\square (A\lor \square B)\to (\square A\lor \square B).$
Well, axiom K says $\square (p\lor q) \to (\lozenge p\lor \square q),$ so as an instance of this, $\square(A\lor \square B)\to (\square A\lor\lozenge \square B).$ But recall from what I said at the outset, that $\lozenge \square B\leftrightarrow \square B,$ so we're done.