Proving tautologies with $\iff$ I have a question regarding the process of proving that a statement form with $\!\iff\!$ is a tautology. For a simple example, let's say we have a statement:
$ (A \iff (B\implies A))$
To attempt to prove that this is a tautology we assume that the statement form is false and try to obtain a contradiction. So if we do assume this then we have two choices, either the left side is true and the right side is false or vice-versa. 
If the left side is true, then A is true, but to make the right side false A would have to be false and B true, therefore we have a contradiction since A cannot be both true and false.
If the left side is false, then A is false, but now for the right side to be true we just let B be false and the right side is true. Therefore in this case the statement form is false when A and B are both false.
Therefore the statement is not a tautology.
Am I correct in my assumption that to prove tautologies with statement forms that use $\iff\!\!$, we must always check both choices for left and right sides? Is there a quicker way to prove that statements such as these are tautologies?
 A: You're correct, you do have to check two things, in any case. But you have two choices about which two things to check.
$p\iff q$ is equivalent to $(p \land q) \lor (\neg p \land \neg q)$. The two disjuncts are the two things you checked: $(p \land q)$, and $(\neg p \land \neg q)$. The two formulas on either side of $\!\iff\!$ have to have the same truth value — either both true, or both false.
The other way to establish a biconditional is to note that $p\!\iff\! q$ is also equivalent to $(p \!\implies\! q) \land (q \!\implies\! p)$. So if you can prove that each of $p$ and $q$ implies the other, then you have proved $p\!\iff\! q$. Note that $p\!\implies\! q$ is true whenever the truth value of $p$ is $\le$ the truth value of $q$. Once again, you prove that the two truth values are equal, but here you do so by showing that they're less than or equal to each other. A variation on this approach is to prove $(p \!\implies\! q) \land (\neg p \!\implies\! \neg q)$, as the second conjunct of that is equivalent to $(q \!\implies\! p)$ (it's the contrapositive of the latter).
