Modus ponens: from a -> b and a, infer b.
a -> b
a
b
axiom ax_mp (a b: wff): $ a -> b $ > $ a $ > $ b $;