By virtue of Proposition 3.1.7.1, the morphism $f_{\overline{B} B}: \overline{B} \rightarrow B$ factors as a composition $\overline{B} \xrightarrow {w} \overline{B}' \xrightarrow { f_{\overline{B} B}' } B$, where $w$ is anodyne and $f_{ \overline{B} B }'$ is a Kan fibration. Replacing $\overline{B}$ by $\overline{B}'$ (and $\overline{D}$ by the pushout $\overline{B}' \coprod _{ \overline{B} } \overline{D}$), we can reduce to the case where $f_{\overline{B} B}$ is a Kan fibration. Similarly, we can arrange that the map $f_{\overline{C} C}: \overline{C} \rightarrow C$ is a Kan fibration.
Applying Proposition 3.1.7.1 again, we can factor the morphism $g: \overline{A} \rightarrow A \times _{ (B \times C) } ( \overline{B} \times \overline{C} )$ as a composition
\[ \overline{A} \xrightarrow {w} \overline{A}' \xrightarrow {g'} A \times _{ (B \times C) } ( \overline{B} \times \overline{C} ), \]
where $w$ is anodyne and $g'$ is a Kan fibration. Replacing $\overline{A}$ by $\overline{A}'$, we can reduce to the case where $g$ is a Kan fibration, so that the morphism $f_{ \overline{A} A}$ is also a Kan fibration.
By virtue of Exercise 3.1.7.11, the morphism $f_{AB}$ factors as a composition $A \xrightarrow { f_{AB}' } B' \xrightarrow {w} B$, where $f_{AB}'$ is a monomorphism and $w$ is a trivial Kan fibration. Replacing $B$ by $B'$ (and $\overline{B}$ by the fiber product $B' \times _{B} \overline{B}'$), we can reduce to the case where $f_{AB}$ is a monomorphism. Similarly, we may assume that $f_{AC}$ is a monomorphism.
By virtue of Exercise 3.1.7.11, the morphism $f_{\overline{A} \overline{B}}$ factors as a composition $\overline{A} \xrightarrow { f_{\overline{A} \overline{B}}' } \overline{B}' \xrightarrow {w} \overline{B}$, where $f_{\overline{A} \overline{B}}'$ is a monomorphism and $w$ is a trivial Kan fibration. Replacing $\overline{B}$ by $\overline{B}'$, we can reduce to the case where $f_{ \overline{A} \overline{B} }$ is a monomorphism. Similarly, we can assume that $f_{ \overline{A} \overline{C}}$ is a monomorphism.
The back face
3.54
\begin{equation} \label{equation:mather-first-cube3} \begin{gathered} \xymatrix@R =50pt@C=50pt{ \overline{A} \ar [r]^-{ f_{ \overline{A} \overline{B} }} \ar [d]^{ f_{\overline{A} A}} & \overline{B} \ar [d]^{ f_{ \overline{B} B} } \\ A \ar [r]^-{f_{AB}} & B } \end{gathered} \end{equation}
is a homotopy pullback square in which the horizontal maps are monomorphisms and the vertical maps are Kan fibrations. It follows that, for every vertex $a \in A$ having image $b = f_{AB}(a) \in B$, the induced map of fibers $\overline{A}_{a} \rightarrow \overline{B}_{b}$ is a homotopy equivalence. Let $\overline{B}' \subseteq \overline{B}$ denote the simplicial subset spanned by those simplices $\sigma : \Delta ^{n} \rightarrow \overline{B}$ having the property that the restriction $\sigma |_{ A \times _{B} \Delta ^{n} }$ factors through $\overline{A}$. Applying Lemma 3.3.8.4, we deduce that the restriction $f_{ \overline{B} B}|_{ \overline{B}' }: \overline{B}' \rightarrow B$ is also a Kan fibration. Moreover, the inclusion map $\overline{B}' \hookrightarrow \overline{B}$ induces a homotopy equivalence of fibers $\overline{B}'_{b} \hookrightarrow \overline{B}_{b}$, for each vertex $b \in B$. It follows that the inclusion $\overline{B}' \hookrightarrow \overline{B}$ is a weak homotopy equivalence (Corollary 3.3.7.5). Replacing $\overline{B}$ by $\overline{B}'$, we can reduce to the case where the diagram (3.54) is a pullback square. Similarly, we can arrange that the diagram
\[ \xymatrix@R =50pt@C=50pt{ \overline{A} \ar [r]^-{ f_{ \overline{A} \overline{C} }} \ar [d]^{ f_{\overline{A} A}} & \overline{C} \ar [d]^{ f_{ \overline{C} C} } \\ A \ar [r]^-{f_{AC}} & C } \]
is a pullback square.
By assumption, the top and bottom faces
3.55
\begin{equation} \label{equation:mather-first-cube4} \begin{gathered} \xymatrix@R =50pt@C=50pt{ \overline{A} \ar [r] \ar [d]^{ f_{\overline{A} \overline{C}}} & \overline{B} \ar [d] & A \ar [r] \ar [d]^{ f_{AC} } & B \ar [d] \\ \overline{C} \ar [r] & \overline{D} & C \ar [r] & D } \end{gathered} \end{equation}
are homotopy pushout squares. Since $f_{ \overline{A} \overline{C} }$ and $f_{AC}$ are monomorphisms, it follows that the induced maps
\[ \overline{C} \coprod _{\overline{A}} \overline{B} \rightarrow \overline{D} \quad \quad C \coprod _{A} B \rightarrow D \]
are weak homotopy equivalences (Proposition 3.4.2.11). We may therefore replace $D$ by the pushout $C \coprod _{A} B$ and $\overline{D}$ by the pushout $\overline{C} \coprod _{\overline{A} } \overline{B}$, and thereby reduce to the case where the diagrams (3.55) are pushout squares.
Applying Exercise 3.4.4.1 levelwise, we deduce that the front and right faces
3.56
\begin{equation} \label{equation:mather-first-cube5} \begin{gathered} \xymatrix@R =50pt@C=50pt{ \overline{C} \ar [r] \ar [d]^{ f_{\overline{C} C}} & \overline{D} \ar [d]^{ f_{ \overline{D} D}} & \overline{B} \ar [r] \ar [d]^{ f_{\overline{B} B}} & \overline{D} \ar [d]^{ f_{\overline{D} D}} \\ C \ar [r] & D & B \ar [r] & D } \end{gathered} \end{equation}
are pullback squares in the category of simplicial sets. In particular, for every simplex $\sigma : \Delta ^ n \rightarrow D$, the projection map $\Delta ^ n \times _{ D} \overline{D} \rightarrow \Delta ^ n$ is a pullback either of $f_{ \overline{B} B}$ or of $f_{ \overline{C} C}$, and is therefore a Kan fibration. Applying Remark 3.1.1.7, we conclude that $f_{ \overline{D} D}: \overline{D} \rightarrow D$ is a Kan fibration. It follows that the diagrams (3.56) are also homotopy pullback squares, as desired.