Consider a category has all finite pullbacks. I want to check $A\times_B(B\times_C D)\cong A\times_C D$.
It is clear from universal property of pullback that I get a unique map $A\times_B(B\times_C D)\to A\times_C D$ by stacking 2 pullback diagrams.
To get $A\times_C D\to A\times_B(B\times_C D)$, it suffices to observe $A\to B$ map giving the opposite morphism on the factor by restricting to the image of $A\times_C D\to A$ projection map. All only commutativity of diagram remains to be checked.
$\textbf{Q:}$ It seems that I have adopted element-wise checking approach for constructing such a map. Is there categorical approach to proving the statement without invoking element-wise checking?(Apparently, this procedure does not work over general category.)