Help with question from Chiswell and Hodges I'm working through Mathematical Logic by Chiswell and Hodges and I'm confused by exercise 2.5.1(d) (pg. 23).
Give derivations to prove the following sequents:
.
.
.
(d) $((A \leftrightarrow (B \leftrightarrow C)) \leftrightarrow ((A \leftrightarrow B) \leftrightarrow C))$
I see that it's clearly true, but the proof I'm finding is about 5 times longer than the proofs for any of the other exercises so far in the book (and a little further). Is there something I'm missing?
 A: 
For : $(A↔(B↔C)) \vdash ((A↔B)↔C)$

First part :
1) $(A↔(B↔C))$ --- premise
2) $C$ --- assumed [a]
3) $A$ --- assumed [b]
4) $B \to A$ --- from 3) by $\to$-intro
5) $A \to (B↔C)$ --- from 1) by $↔$-elim
6) $(B↔C)$ --- from 3) and 5) by $\to$-elim
7) $C \to B$ --- from 6) by $↔$-elim
8) $B$ --- from 2) and 7) by $\to$-elim
9) $A \to B$ --- from 3) and 8) by $\to$-intro, discharging [b]
10) $(A↔B)$ --- from 4) and 9) by $↔$-intro

11) $C \to (A↔B)$ --- from 2) and 10) by $\to$-intro, discharging [a].


Second part (this is the only way I've found):
1) $(A↔(B↔C))$ --- premise
2) $(A↔B)$ --- assumed [a]
3) $A \lor \lnot A$ --- Excluded Middle
4) $A$ --- assumed [b] (for $\lor$-elim)
5) $A \to B$ --- from 2)
6) $B$ --- from 4) and 5)
7) $(B↔C)$ --- from 4) and 1) 
8) $B \to C$ --- from 7)
9) $C$ --- from 6) and 8)
10) $\lnot A$ --- assumed [c] (for $\lor$-elim)
11) $B$ --- assumed [d]
12) $C \to B$ --- from 11) by $\to$-intro
13) $B \to A$ --- from 2)
14) $A$ --- from 11) and 13)
15) $\bot$ --- from 10) and 14)
16) $C$ --- from 15)
17) $B \to C$ --- from 11) and 16) by $\to$-intro, discharging [d]
18) $(B↔C)$ --- from 12) and 17)
19) $A$ --- from 1) and 18) by $↔$-elim and $\to$-elim
20) $\bot$ --- from 10) and 19)
21) $C$ --- from 20)
22) $C$ --- from 4)-9) and 10)-21) and 3) by $\lor$-elim, discharging [b] and [c]

23) $(A↔B) \to C$ --- from 2) and 22) by $\to$-intro, discharging [a].




$(A↔B) ↔ C$ --- from 11) and 23) by $↔$-intro.


A: In my opinion, the presence of 2.5.9. (d) in its place in the book is a mistake. By the end of section 2.5, one knows only the following rules of deduction:
(∧I), (∧E), (→I), (→E), (↔I), (↔E)
It is impossible to do with such a limited toolset. This impossibility can be proven using the method of exercise 3.9.2, using three-value logic as normally in 3.9.2 with additional definitions:
A*((φ∧ψ)) = min(A*(φ),A*(ψ))
A*((φ↔ψ)) = A*((φ→ψ)∧(ψ→φ))
And showing that adding rules (∧I), (∧E),(↔I), (↔E) does not affect the validity of the claim in exercise 3.9.2 step (c).
Then, let's  assume A*(φ) = A*(ψ) = 0 and A*(χ) = 1/2. The A* value of the whole formula from 2.5.9(d) equals 1/2, which is less than 1, so any derivation of this formula using only the toolset one knows by finishing reading section 2.5 would need an undischarged assumpiton.
