Understanding Symbolic Logic, Virginia Klenk, 5th edition, Pearson Prentice Hall, Unit 20, Ex. 3(d)

The theorem to prove this time requires little beyond the application of the transitive property of identity.

Theorem: (x)(y)(z)(w)[(x = y • y = z • z = w) ⊃x = w]

1. * x = y / ACP
2. * * y = z / ACP
3. * * * z = w / ACP
4. * * * x = z / 1,2HS
5. * * * x = w / 4,3HS
6. * * z = w ⊃x = w / 3-5CP
7. * y = z ⊃(z = w ⊃x = w) / 2-6CP
8. x = y ⊃[y = z ⊃(z = w ⊃x = w)] / 1-7CP
9. (x = y • y = z • z = w) ⊃x = w / 8Exp.
10. (w)[(x = y • y = z • z = w) ⊃x = w] / 9UG
11. (z)(w)[(x = y • y = z • z = w) ⊃x = w] / 10UG
12. (y)(z)(w)[(x = y • y = z • z = w) ⊃x = w] / 11UG
13. (x)(y)(z)(w)[(x = y • y = z • z = w) ⊃x = w] / 12UG