Theory of proveit.logic.booleans.implication¶
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$.
