Prove $\vdash \neg(A\equiv B) \equiv \neg A\equiv B$ I'm having a hard time understanding how to prove this: here is the proof I've read - however I understand that this is actually proving $(B\equiv \bot) \vdash \neg(A\equiv B) \equiv \neg A\equiv B$: 
$$\neg(A\equiv B)$$
<=> (axiom)
$$(A\equiv B)\equiv \bot$$
<=> (Leib + axiom: $B\equiv \bot \equiv \bot \equiv B$; 'C-part' is $A\equiv p$)
Question: How come I can use $B\equiv \bot$ in an axiom?
$$A\equiv \bot \equiv B$$
<=> (Leib + axiom: $A\equiv \bot \equiv \neg A$; 'C-part' is $p\equiv B$)
$$\neg A \equiv B$$
 A: $\vdash X\equiv X$ by rule of identity.  (Equivalence is reflexive).
$\lnot X$ is equivalent to $X\equiv \bot$, by the definition of negation and falsity.   $\lnot X$ says "$X$ is false", which is to say $X\equiv\bot$.
$(X\equiv Y)\equiv Z$ is equivalent to $X\equiv (Y\equiv Z)$ because the biconditional operator is associative.   Since there is thus no ambiguity about order of association, we often express these as also being equivalent to $X\equiv Y\equiv Z$ .
The biconditional operator is also commutative, so $X\equiv Y$ is equivalent to $Y\equiv X$.
Now, applying these rules as substitutions.
$$\begin{align}&\vdash \lnot (A\equiv B)\equiv\lnot(A\equiv B) &&\text{by Identity}\\&\vdash \lnot (A\equiv B)\equiv ((A\equiv B)\equiv\bot)&&\text{by definition of negation}\\&\vdash \lnot (A\equiv B)\equiv (A\equiv (B\equiv\bot))&&\text{by association}\\&\vdash \lnot (A\equiv B)\equiv (A\equiv (\bot\equiv B))&&\text{by commutation}\\&\vdash \lnot (A\equiv B)\equiv ((A\equiv \bot)\equiv B)&&\text{by association}\\&\vdash \lnot (A\equiv B)\equiv (\lnot A\equiv B)&&\text{by definition of negation}\\&\vdash \lnot (A\equiv B)\equiv \lnot A\equiv B&&\text{by unambiguous association} \end{align}$$
A: The proof uses Equational logic (see also this post for details).
We start form the premise :

1) $¬(A≡B)$

and we want to transform it (through equivalences) into the conclusion.
The first step uses the axiom defining $\lnot$ : $\lnot A \equiv (A \equiv \bot)$ to get :
2) $(A≡B) \equiv \bot$.
The next step uses associativity of $\equiv$ to get :
3)  $A≡ (B \equiv \bot)$.
Now we use Leibniz's rule : 

from $D_1 \equiv D_2$ and $C[p:=D_1]$ derive $C[p:=D_2]$, where $C$ is a formula and $C[p:=D_i]$ is obtained from $C$ replacing part $p$ with formula $D_i$, 

with axiom for symmetry of $\equiv$ : $(B \equiv \bot) \equiv (\bot \equiv B)$.
This means to use the axiom as $C$ and $(B \equiv \bot)$ as $D_1$ and $A$ as $D_2$, to get :
4) $A \equiv (\bot \equiv B)$.
Apply associativity again to get :
5) $(A \equiv \bot) \equiv B$
and finally use Leibniz again with the axiom for $\lnot$ to replace $(A \equiv \bot)$ in 5) with $\lnot A$ to conclude with :


6) $\lnot A \equiv B$.


