Implication [GS]

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)