Theory for implication operations:
Implies ($\Rightarrow$) and
Iff ($\Leftrightarrow$). The
Implies operation has an
antecedent and a
consequent. For example, in $A \Rightarrow B$, $A$ is the
antecedent and $B$ is the
consequent. If an implication is true and the
antecedent is true (e.g., $A$), the
consequent must also be true (e.g. $B$). That is $B$ is true if $A$ is true.
Iff should be read "if and only if" and is defined to mean that the implication goes both ways. That is $A \Leftrightarrow B$ means $A \Rightarrow B$ and $B \Rightarrow A$.
import proveit %theory