This is a proof of

|- (Øp º p) º false

which is (3.15) where P is p. Typically, (3.1) and (3.1)¢ are used transparently. In this proof, detail concerning their use is explictly given.

(Øp º p) º false = á (3.8) and Leibniz where E is (Øp º p) º r gives |- ((Øp º p) º false) º ((Øp º p) º Øtrue). ñ (Øp º p) º Øtrue = á (3.2) where P is Øp and Q is p and Leibniz where E is r º Øtrue gives |- ((Øp º p) º Øtrue) º ((p º Øp) º Øtrue). ñ (p º Øp) º Øtrue = (3.1) where P is p, Q is Øp, and R is Øtrue. p º (Øp º Øtrue ) = á (3.11) where P is p and Q is Øtrue and Leibniz where E is p º r gives |- (p º (Øp º Øtrue)) º (p º (p º ØØtrue)). ñ p º (p º ØØtrue) = á (3.12) where P is true and Leibniz where E is p º (p º r) gives |- (p º (p º ØØtrue)) º ( p º (p º true)). ñ p º (p º true) = (3.1)¢ where P is p, Q is p and R is true. (p º p) º true = á (3.3) where P is p and Leibniz where E is (p º p ) º r gives |- ( (p º p) º true) º ((p º p)    º   (p º p) ). ñ (p º p)    º   (p º p)  .

Transitivity applied four times gives

|- ((Øp º p) º false)     º     ((p º p)    º   (p º p)) .

But (3.5) where P is p º p gives |- (p º p)    º   (p º p) . By Equanimity,

|- Øp º p º false  .

Note that the use of Transitivity four times and Equanimity once can be replaced by the use of Equanimity five times.
Note that (3.1)¢ is the Axiom Scheme

|-  (P º (Q º R))    º   ((P º Q) º R)  .