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?
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
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]