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$.

In [1]:

```
import proveit
%theory
```