I am trying to prove the Conditional Exchange:
$$(P \implies Q) \iff (\neg P \lor Q)$$
Sadly, I can't provide an attempt because, well, I'm not quite sure where to start. I can't see any way to use a direct proof, so possibly an assumption of some form might be the best course of action. My biggest problem is how to get from the Conditional to the disjunction. Is there some property or rule that I'm forgetting or don't know? To my knowledge, the Conditional Exchange is the only way to "get" from Conditional to disjunction.
And yes, I've constructed a truth table for this before. I'm trying to find a formal proof.
Here is a proof of going from the conditional to the disjunction in the system I like to use myself: