theorem ancomb (a b: wff): $ a /\ b <-> b /\ a $;
a /\ b -> b /\ a
b /\ a -> a /\ b
a /\ b <-> b /\ a