If your predicate has an implication in it, sometimes it's easier to work with the equivalent disjunctive formulation:
Here are some other useful properties about implication and boolean constants:
(Reflexivity)(Right zero)
(Left identity)
Here are some useful theorems about implication:
(Shunting)