How to prove this: ¬C → B , C → ¬B ⊢ ¬B ↔ C in TFL with natural deduction? I'm really stuck on how to prove ¬C → B , C → ¬B ⊢ ¬B ↔ C. I know I have $C \implies \sim B$ but in order to introduce the biconditional I have to prove $\sim B \implies C$ and I have no idea how. Any help is greatly appreciated. So far this is what I have:

*

*$\quad \sim C \implies B :PR$


*$\quad C \implies \sim B :PR$


*$\quad \sim B :AS$


*$\quad ?????$


*$\quad \sim B \implies C :\implies I\;(???)$


*$\quad \sim B \iff C : \iff I2,5$
 A: Using TFL's fundamental rules, here's a derivation for $C\to\neg B\vdash_{\tiny\!\! TFL} B\to\neg C$ :
$$\def\fitch#1#2{~~~~\begin{array}{|l}#1\\\hline#2\end{array}}\fitch{~~1.~C\to\neg B}{\fitch{~~2.~B}{\fitch{~~3.~C}{~~4.~\neg B\qquad{\to}E~1,3\\~~5.~\bot~~\qquad\neg E~4,2}\\~~6.~\neg C\qquad\neg I~3{-}5}\\~~7.~B\to\neg C\qquad{\to}I ~2{-}6}$$
The derivation you want is similar.
$$\fitch{~~1.~\neg C\to B}{\fitch{~~2.~\neg B}{~~~~\vdots\\~~7.~C}\\~~8.~\neg B\to C\qquad{\to}I ~2{-}7}$$
A: Heres one potential way to do it,
$$\begin{align}
\neg C \to B , C \to \neg B, C &\vdash C &&\text{($\in$)}\\
\neg C \to B , C \to \neg B, C &\vdash C \to \neg B &&\text{($\in$)}\\
\neg C \to B , C \to \neg B, C &\vdash \neg B &&\text{($\to -$), (1), (2)}\\
\neg C \to B , C \to \neg B, \neg B, \neg C &\vdash \neg B &&\text{($\in$)}\\
\neg C \to B , C \to \neg B, \neg B, \neg C &\vdash \neg C &&\text{($\in$)}\\
\neg C \to B , C \to \neg B, \neg B, \neg C &\vdash \neg C \to B &&\text{($\in$)}\\
\neg C \to B , C \to \neg B, \neg B, \neg C &\vdash B &&\text{($\to -$), (5), (6)}\\
\neg C \to B , C \to \neg B, \neg B &\vdash C &&\text{($\neg -$), (4), (7)}\\
\neg C \to B , C \to \neg B &\vdash \neg B \leftrightarrow C &&\text{($\leftrightarrow +$), (3), (8)}
\end{align}$$
