Forming a propositional formula from recursive statements I'm having trouble combining/forming a single propositional formula from 3 recursively expressed statements. The original setting of the problem is something like:
There are three people $A$, $B$ and $C$. 


*

*$A$ said: $B$ and $C$ told the truth if and only if $C$ told the truth.

*$B$ said: If $A$ and $C$ told the truth, then it is not the case that: if $B$ and $C$ told the truth, then $A$ told the truth.

*$C$ said: $B$ did not tell the truth if and only if $A$ or $C$ told the truth.
From the statements I was able to formulate 3 propositional formulas for each person. I used $T_A$, $T_B$ and $T_C$ to represent the variables for the statements of each candidate, if they were true. That is,


*

*for $A$: $T_A \Leftrightarrow ((T_B \land T_C) \Leftrightarrow T_C)$ 

*for $B$: $T_B \Leftrightarrow ((T_A \land T_C) \Rightarrow \lnot ((T_B \land T_C) \Rightarrow T_A))$ 

*for $C$: $T_C \Leftrightarrow ((T_A \lor T_C) \Leftrightarrow \lnot T_B)$ 
Now I am supposed to combine the 3 formulas above to a single one. My thought is after doing this, we could enumerate what would the value of the whole formula be for all the possible values of $T_A$, $T_B$ and $T_C$. If the whole formula turned out to be $true$ somewhen, then we could tell who actually lies judging from the value of $T_A$, $T_B$ and $T_C$. 
I'm stuck here because the statements are recursive. I assume the 3 formulas I wrote above are correct. (Please correct me if I was wrong!) I was kind of always chasing my tail and didn't come up with a solution. 
How should I combine the above 3 formulas correctly? 
Thanks in advance.
 A: Combining three formulas is surprisingly straightforward - you have three formulas that must simultaneously be true, so you want to put an $\wedge$ between them. So your final formula would be $(T_A \iff ((T_B \wedge T_C) \iff T_C)) \wedge (T_B \iff ((T_A \wedge T_C) \Rightarrow \neg((T_B \wedge T_C) \Rightarrow T_A))) \wedge (T_C \iff ((T_A \vee T_C) \iff \neg T_B))$.
A: HINTS


*

*Whenever you have $\varphi \leftrightarrow \psi$, and you have some other statement that involves $\varphi$'s, then you can substitute $\psi$'s for those $\varphi$'s in the other sentence.  Or, as a general principle:


$(\varphi \leftrightarrow \psi) \land S(\varphi) \Leftrightarrow (\varphi \leftrightarrow \psi) \land S(\psi)$
where $S(\varphi)$ is a sentence containing any number of $\varphi$'s, and  $S(\psi)$ is the result of substituting any number of those $\varphi$'s with $\psi$'s.
So in your case, you can go from:
$(T_A \Leftrightarrow ((T_B \land T_C) \Leftrightarrow T_C)) \land $
$(T_B \Leftrightarrow ((T_A \land T_C) \Rightarrow \lnot ((T_B \land T_C) \Rightarrow T_A))) \land $
$(T_C \Leftrightarrow ((T_A \lor T_C) \Leftrightarrow \lnot T_B))$ 
to:
$(T_A \Leftrightarrow ((T_B \land T_C) \Leftrightarrow T_C)) \land $
$(T_B \Leftrightarrow ((((T_B \land T_C) \Leftrightarrow T_C) \land T_C) \Rightarrow \lnot ((T_B \land T_C) \Rightarrow ((T_B \land T_C) \Leftrightarrow T_C)))) \land $
$(T_C \Leftrightarrow ((((T_B \land T_C) \Leftrightarrow T_C) \lor T_C) \Leftrightarrow \lnot T_B))$ 


*You can do some simplifications (and I'll write $A$ for $T_A$ to save some typing):


$(B \land C) \leftrightarrow C \Leftrightarrow$ (rewrite $\leftrightarrow$)
$((B \land C) \land C) \lor (\neg (B \land C) \land \neg C)) \Leftrightarrow$ (Association, DeMorgan)
$(B \land (C \land C)) \lor ((\neg B \lor \neg C) \land \neg C))\Leftrightarrow $ (Idempotence, Absorption)
$(B \land C) \lor \neg C)\Leftrightarrow$ (Reduction)
$B \lor \neg C$
Also: $\neg ((B \land C) \rightarrow A) \Leftrightarrow (B \land C) \land \neg A$
