One quite useful application of this is that implication can play the role of the partial-order operator in a Galois Connection. A Gallois connection is an iff-and-only-if formula of the form

    F(x) ≤ y  iff x ≤ G(y)

One form of this is the tautology when F(x) = (x and a), G(y) = (a => y), and pick logical implication as the "≤".

    ((x and a) => y) iff (x => (a => y))

https://en.wikipedia.org/wiki/Galois_connection#Power_set;_i...