Description: Conjunction distributes over exclusive-or, using -. ( ph <-> ps ) to
express exclusive-or. This is one way to interpret the distributive law
of multiplication over addition in modulo 2 arithmetic. This is not
necessarily true in intuitionistic logic, though anxordi does hold in
it. (Contributed by NM, 3-Oct-2008)