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