theorem anl (a b: wff): $ a /\ b -> a $;
(~a -> a -> ~b) -> ~(a -> ~b) -> a
(~a -> a -> ~b) -> a /\ b -> a
~a -> a -> ~b
a /\ b -> a