Reductio Ad Absurdum Question I've been stuck on this question (which uses RAA). Was wondering if somebody could help me to make sense of it?
$$\{\neg (\phi \leftrightarrow \psi )\} \vdash ((\neg \phi )\leftrightarrow \psi )$$
Thanks
 A: HINT: Apply the Deduction theorem. Twice.
A: So I'm not sure which natural deduction system you're using or if you're using a sequent calculus.  I use Polish notation.  I'll also use lower case Latin letters than Greek letters.  We want to show NEpq $\vdash$ ENpq.  X-in stands for an introduction rule for connective X.  X-out stands for an elimination rule for connective X.
  1      NEpq assumption
  2 |    Np hypothesis
  3 ||   Nq hypothesis
  4 |||  p hypothesis
  5 |||| Nq hypothesis
  6 |||| KpNp 4, 2 K-in
  7 |||  q  5-6 RAA
  8 ||   Cpq 4-7 C-in
  9 |||  q hypothesis
 10 |||| Np hypothesis
 11 |||| KqNq 9, 3 K-in
 12 |||  p 10-11 RAA
 13 ||   Cqp 9-12 C-in
 14 ||   Epq 8, 13 E-in
 15 ||   KEpqNEpq 1, 14 K-in
 16 |    q 3-15 RAA
 17      CNpq 2-16 C-in
 18 |    q hypothesis
 19 ||   NNp hypothesis
 20 |||  Np  hypothesis
 21 |||  KNpNNp 20, 19 K-in
 22 ||   p   20-21 RAA
 23 |||  q hypothesis
 24 |||| p hypothesis
 25 |||  Cpp 24-24 C-in
 26 |||  p  25, 22 C-out
 27 ||   Cqp 23-26 C-in
 28 |||  p hypothesis
 29 |||| q hypothesis
 30 |||  Cqq 29-29 C-in
 31 |||  q 18, 30 C-out
 32 ||   Cpq 28-31 C-in
 33 ||   Epq 27, 32 E-in
 34 ||   KEpqNEpq 1, 33 K-in
 35 |    Np 19-34 RAA
 36      CqNp 18-35 C-in
 37      ENpq 17, 36 E-in

