How to Prove $((F \iff H) \iff ((\neg F \land \neg H) \lor (F \land H)))$ I am at a complete loss here... 
$(F \iff H)$ PREMISE
...
$((\neg F \land \neg H) \lor (F \land H))$ GOAL
I keep getting stuck in a loop of contradiction and not able to complete the proof.
I can use the following rules to complete the proof: Conjunction Introduction, Conjunction Elimination, Disjunction Introduction, Disjunction Elimination, Conditional Introduction (although not applicable here), Conditional Elimination (also not applicable), Negation Introduction, Falsum Introduction, Negation Elimination, Biconditional Introduction, and Biconditional Elimination. 
For example: I can apply Disjunction Introduction Left ("$\lor IL$") to the current GOAL and result with either (F∧H) or (¬F∧¬H) which then becomes the new goal, such as this:
$(F \iff H)$ PREMISE
...
$(F \land H))$ GOAL
$((\neg F \land \neg H) \lor (F \land H))$ 
Thoughts?
 A: I'm not sure if this proof uses the right system, but perhaps it will help you. It uses the rules of replacement typically called equivalence, implication, and distribution (twice), plus the fact that $p \lor (q \wedge \neg q) \rightarrow p$:
\begin{align*}
(F \leftrightarrow H) &\Leftrightarrow (F \rightarrow H) \wedge (H \rightarrow F) \\
&\Leftrightarrow (\neg F \lor H) \wedge (\neg H \lor F)\\
&\Leftrightarrow ((\neg F \lor H) \wedge \neg H ) \lor ((\neg F \lor H) \wedge F) \\
&\Leftrightarrow ((\neg F \wedge \neg H) \lor (H \wedge \neg H)) \lor ((\neg F \wedge F) \lor (H \lor F)) \\
&\Leftrightarrow (\neg F \wedge \neg H) \lor (H \wedge F) \\
&\Leftrightarrow (\neg F \wedge \neg H) \lor (F \wedge H)
\end{align*}
A: (F↔H) 
   ¬ ((¬F∧¬H) ∨ (H∧F)) 
      ¬ (¬F∧¬H) 
         F 
         H 
         (F ∧ H) 
         ((¬F∧¬H) ∨ (H∧F)) 
         ┴ 
      ¬F 
         H 
         F 
         (F ∧ H) 
         ((¬F∧¬H) ∨ (H∧F)) 
         ┴ 
      ¬H 
      (¬F∧¬H) 
      ┴ 
   (¬F∧¬H) 
   ((¬F∧¬H) ∨ (H∧F)) 
   ┴ 
((¬F∧¬H) ∨ (H∧F)) 
A: You can complete a table of values for both expressions. Completion of the table will certainly use the given rules.
A: Note that one might intuitively expect this result to be an equivalence:
$$(F\leftrightarrow H) \equiv (\neg F \land \neg H) \lor (F \land H)$$
If $F$ and $H$ are equivalent then when $F$ is false, $H$ will also be false. That is represented by $\neg F \land \neg H$. Similarly when $F$ is true, $H$ will be true which is represented by $F \land H$. One of these two cases will occur so one can connect them with a disjunction ($\lor$).
However, to make sure, here is a natural deduction proof using a Fitch-style proof checker.  This uses the law of the excluded middle as was used in the OP's proof and considers both directions in showing the equivalence.


Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/
