In [1]:

```
import proveit
# Prepare this notebook for defining the axioms of a theory:
%axioms_notebook # Keep this at the top following 'import proveit'.
from proveit.logic import Equals, Implies, TRUE, FALSE, Forall, And, Iff, Not, NotEquals, Boolean
from proveit import A, B
%begin axioms
```

In [2]:

```
implies_t_f = Equals(Implies(TRUE, FALSE), FALSE)
```

In [3]:

```
affirmation_via_contradiction = Forall(A, A, domain=Boolean, conditions=[Implies(Not(A), FALSE)])
```

In [4]:

```
denial_via_contradiction = Forall(A, Not(A), domain=Boolean, conditions=[Implies(A, FALSE)])
```

`Iff`

(if and only if) is defined as implication in both directions:

In [5]:

```
iff_def = Forall((A, B), Equals(Iff(A, B), And(Implies(A, B), Implies(B, A))))
```

In [6]:

```
%end axioms
```