We introduce a new type of proof formalism for multiagent modal logics with S5-type modalities, viewed here as a logic of multiagent epistemic reasoning, and use this formalism to give a constructive proof that multiagent S5 enjoys a strong form of Craig interpolation with respect to both propositional variables and agents, the latter in the form of agent-indexed knowledge modalities. Our new proof formalism combines the features of hypersequents to represent S5 modalities with nested sequents to represent the T-like modality alternations. Combining these features is necessary to obtain computationally effective interpolation for agents rather than merely propositional variables, and we further show that our new proof formalism is sound and complete, cut-free, strongly terminating, and yields decidability and the finite model property for multiagent S5.