Propositional Logic, Howard Pospesel, Prentice Hall, 2000, 3rd edition, Chapter 9, ex. 22

The task is to prove that the biconditional is associative. The hardest thing is to think of the correct assumptions to get us started. Eventually, two assumptions for conditional proof and two for indirect proof are used before we can begin to unpick line 4.

1. C ≡ (D ≡ E)
2. ∴(C ≡ D) ≡ E
3. [C ⊃(D ≡ E)] [(D ≡ E) ⊃C] / 2BE
4. {C ⊃[(D ⊃E) • (E⊃D)]} • {[(D⊃E) • (E⊃D)] ⊃C} / 3BE
5. * C ⊃D / ACP
6. * * D ⊃C / ACP
7. * * * ¬ E / AIP
8. * * * * ¬ D / AIP
9. * * * * ¬ C / 8,5MT
10. * * * * [(D⊃E) • (E⊃D)] ⊃C / 4Simp.
11. * * * * ¬ [(D⊃E) • (E⊃D)] / 9,10MT
12. * * * * [ ¬ (D⊃E) ∨¬ (E⊃D)] / 11DeM
13. * * * * ¬ D ∨E / 8Add
14. * * * * ¬ (D • ¬ E) / 13DeM
15. * * * * (D • ¬ E) ∨(E • ¬ D) / 12DeM
16. * * * * E • ¬ D / 14,15DS
17. * * * * E / 16Simp.
18. * * * * E • ¬ E / 7,17Conj.
19. * * * ¬ ¬ D / 8-18IP
20. * * * D / 19DN
21. * * * C / 6,20MP
22. * * * C ⊃[(D ⊃E) • (E⊃D)] / 4Simp.
23. * * * (D ⊃E) • (E⊃D) / 21,22MP
24. * * * D ⊃E / 23Simp.
25. * * * ¬ D / 7,24MT
26. * * * ¬ D • D / 20,25Conj.
27. * * ¬ ¬ E / 7,26IP
28. * * E / 27DN
29. * (D ⊃C) ⊃E / 6-28CP
30. (C ⊃D) ⊃[(D ⊃C) ⊃E] / 5-29CP
31. [(C ⊃D) • (D ⊃C)] ⊃E / 30Exp
32. * E / ACP
33. * * C / ACP
34. * * C ⊃[(D ⊃E) • (E⊃D)] /4Simp.
35. * * (D ⊃E) • (E⊃D) / 33,34MP
36. * * E⊃D / 35Simp.
37. * * D / 32,36MP
38. * C ⊃D / 33-37CP
39. * * D / ACP
40. * * D ∨¬ E / 37Add
41. * * E ⊃D / 40CE or MI
42. * * E ∨¬ D / 32Add
43. * * D ⊃E / 42CE or MI
44. * * (D ⊃E) • (E ⊃D) / 41,43Conj.
45. * * [(D⊃E) • (E⊃D)] ⊃C / 4Simp.
46. * * C / 44,45MP
47. * D ⊃C / 39-46CP
48. * (C ⊃D) • (D ⊃C) /38,47Conj.
49. E ⊃[(C ⊃D) • (D ⊃C)] / 32-48CP
50. {[(C ⊃D) • (D ⊃C)] ⊃E} • {E ⊃[(C ⊃D) • (D ⊃C)]} / 31,49Conj.
51. [(C ≡ D) ⊃E] • [E⊃(C ≡ D)] / 50BE
52. (C ≡ D) ≡ E / 51BE