 
  
  
   
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)

