How to proof logic with axioms and modus ponens? My last question was about how to derive Truth Tables from a given logic statement. Now that I think i can manage I have been bestowed with a new quest in my search of mathematical enlightenment. This quest comes from the awesome Logic in Action book/pdf that can be found here page 2-23, example 2.25:

So I need to invite people (I guess the most people).
So the most people are Mary and John, where Ann does not come.
so:

Ann comes, John does not
  $$ a \rightarrow \neg j $$
  Ann comes if Mary does not come
  $$ \neg m \rightarrow a $$
  John comes if Mary or Ann comes
  $$ a \rightarrow j $$
  $$ m \rightarrow j $$

So to prove that when Ann does not come Mary and John do come I started with this:
Let's say that John does not come.
$$ a \rightarrow \neg j $$
$$ \neg m \rightarrow a $$
This conclusion tells me that Ann does not come, or she would be the only person invited. So Ann must be false
$$ \neg a $$
Next is to see if Mary or John comes.
$$ \neg a \rightarrow j $$ 
$$ m \rightarrow j $$
$$ \neg a \rightarrow m $$
Mary comes, because Ann does not, therefore John also comes
The question is... Am I doing the proof thing correct?
This is all very new to me, and the book does not explain very well.
ps. some reference to youtube videos that ELI5 would be appreciated.
 A: Given $a \to \neg j$ and the fact that John does not come, the following is incorrect:

This conclusion tells me that Ann does not come, or she would be the
  only person invited. So Ann must be false $\neg a$.

Modus ponens only works with a given antecedent as follows:
\begin{array}{l}
& a & \text{ Given }\\
& a \to \neg j & \text{ Given }\\
& \neg j & \text{ Modus ponens }\\
\end{array}
In other words, there's no variation to this, such as, for example that given the consequent, you can conclude the antecedent. It only works when the antecedent is known, either as a premise or as the consequent of some other argument. When that's the case, you can assert the consequent.
One of the axioms that the text gives is $((\neg \phi \to \neg \psi) \to (\psi \to \phi))$. Applying this, you can conclude $\neg a$ as follows:
\begin{array}{l}
& j & \text{ Premise }\\
& a \to \neg j & \text{ Premise }\\
& j \to \neg a & \text{ Axiom }\\
& \neg a & \text{ Modus ponens }\\
\end{array}
A similar method can be used to conclude $m$, and knowing $m$, it's easy to conclude $j$:
\begin{array}{l}
& \neg a & \text{ Premise }\\
& \neg m \to a & \text{ Premise }\\
& m \to j & \text{ Premise }\\
& \neg a \to m & \text{ Axiom (applied to 2nd premise) }\\
& m & \text{ Modus ponens}\\
& j & \text{ Modus ponens }\\
\end{array}
