# Proving $\neg (p\land \diamond q)$

Assume the Necessitation Rule and the Distribution Axiom (https://en.wikipedia.org/wiki/Modal_logic#Axiomatic_systems) of modal logic, and also assume the axiom $$p\land \diamond q\to \diamond(q\land\diamond p)$$. Suppose that $$\neg(\diamond p\land q)$$ is provable (one can apply all standard inference rules and all tautologies of propositional logic). I'm trying to show that $$\neg (p\land \diamond q)$$ is also provable.

Assume by contradiction $$p\land \diamond q$$. By modus ponens, $$\diamond(q\land\diamond p)$$ or $$\neg \square \neg (q\land \diamond p)$$. We also have $$\neg (q \land \diamond p)$$. But I don't see how to obtain a contradiction.

Since $$\lnot(q\land\lozenge p)$$ is provable, then it is a theorem and the necessitation rule can be applied.