Simple logic question but unsure how to begin How would I go about showing this? Intuitively this is very simple, but I've never been asked to prove an $\iff$ relation with $\iff$ inside of it:
$(A \iff B) \iff (\lnot A \iff \lnot B)$
 A: Rewrite $A\iff B$ as $(A \wedge B)\vee(\lnot A \wedge \lnot B)$ then you will get
$$\begin{array}{rcl}&& (A\iff B) \\
&\iff& \left( (A \wedge B)\vee(\lnot A \wedge \lnot B) \right)\\
&\iff& \left( (\lnot A \wedge \lnot B)\vee( A \wedge B)\right) \\
&\iff& \left(( \lnot A \wedge \lnot B)\vee( \lnot(\lnot A) \wedge \lnot(\lnot B))\right) \\
&\iff& (\lnot A\iff \lnot B)
\end{array}$$
A: It depends on what the basic rules about $\;A \iff B\;$ that you are allowed to use: Is it considered a primitive (as in the 'equational logic' of Dijkstra and Gries-Schneider), or is it an abbreviation for $\;(A \implies B) \land (B \implies A)\;$, as $\;(A \land B) \lor (\lnot A \land \lnot B)\;$, or yet another variation?
If $\;\iff\;$ is a primitive, or in general if you are allowed to use the fact that $\;\iff\;$ is associative (in addition to some other properties), then you can just leave out the parentheses, and calculate
\begin{align}
& A \iff B \;\iff\; \lnot A \iff \lnot B \\
= & \qquad \text{"use symmetry of the middle $\;\iff\;$"} \\
& A \iff \lnot A \;\iff\; B \iff \lnot B \\
= & \qquad \text{"$\;P \iff \lnot P\;$ is always false"} \\
& \text{false} \;\iff\; \text{false} \\
= & \qquad \text{"$\;P \iff P\;$ is always true"} \\
& \text{true} \\
\end{align}
Otherwise, you can use an approach as in the first answer.
A: $(A \iff B)$
$\iff ([A\implies B] \wedge [B \implies A])$ (Definition of $\iff$)
$\iff ([\lnot A \vee B] \wedge [\lnot B \vee A])$ (Equivalence of $\implies$)
$\iff ([\lnot B \vee A] \wedge [\lnot A \vee B])$ (Commutativity of $\wedge$)
$\iff ([A \vee \lnot B] \wedge [B \vee \lnot A])$ (Commutativity of $\vee$)
$\iff ([\lnot A \implies \lnot B] \wedge [\lnot B \implies \lnot A])$ (Equivalence of $\implies$)
$\iff (\lnot A \iff \lnot B)$ (Definition of $\iff$)
