Fiber Product is an embedded submanifold

I'll expand on Dap's answer, at least the way I understood it.

Let $n:=\dim E,\,m:=\dim F,\,k:=\dim B$ and a point $(e,f)\in E\times F$ with $\pi(e)=\phi(f)=:b$.

Informal proof: if $(e,f)$ has local coordinates $(x_1,...,x_n,y_1,...,y_m)$, we may assume $\pi(x_1,...,x_n)=(x_1,...,x_k)$, since $\pi$ is a submersion. So, locally, $E\times_B F$ is made of points $(x_1,...,x_n,y_1,...,y_m)$ with $(x_1,...,x_k)=\phi(y_1,...,y_m)$, i.e., points of the form $(\phi(y_1,...,y_m),x_{k+1},...,x_n,y_1,...,y_m)$. Therefore the coordinates $x_{k+1},...,x_n,y_1,...,y_m$ are just enough to describe $E\times_B F$ locally, which means it's embedded and has dimension $n+m-k$ $\,_\blacksquare$

I think that's convincing enough, but I thought better to check the details:

Formal proof: since $\pi$ is a submersion, we may take charts $(U,\varphi)$ at $e$ and $(V,\psi)$ at $b$ such that $$\psi\circ\pi\circ\varphi^{-1}:(u_1,...,u_n)\mapsto (u_1,...,u_k)$$

i.e., $\psi\circ\pi=(\varphi_1,...\varphi_k)$. Now, for an open $W\subset\phi^{-1}(V)$ we take a chart $(W,\xi)$ at $f$, so for $M:=E\times_B F$ we have: \begin{align*} (U\times W)\cap M&=\{(e,f)\mid \psi\circ \pi(e)=\psi\circ\phi(f)\}\\ &=\{(e,f)\mid (\varphi_1(e),...\varphi_k(e))=\psi\circ\phi(f)\} \end{align*}

If $\hat{\phi}:=\psi\circ\phi\circ\xi^{-1}$, define the map: \begin{align*} g:\varphi(U)\times\xi(W) &\to \mathbb{R}^{n+m}\\ (u_1,...,u_n,v_1,...,v_m) &\mapsto((u_1,...,u_k)-\hat{\phi}(v_1,...,v_m),u_{k+1},...,u_n,v_1,...,v_m) \end{align*} which has an inverse at its image: $$(u_1,...,u_n,v_1,...,v_m)\mapsto((u_1,...,u_k)+\hat{\phi}(v_1,...,v_m),u_{k+1},...,u_n,v_1,...,v_m)$$ This means that for $\chi:=g\circ(\varphi\times \xi)$, we have a chart $(U\times W,\chi)$ and: \begin{align*} \chi((U\times W)\cap M)&=\{g(\varphi(e),\xi(f))\mid (e,f)\in (U\times W)\cap M\}\\ &=\{(u_1,...,u_n,v_1,...,v_m)\in\chi(U\times W)\mid u_1=...=u_k=0\}\,_\blacksquare \end{align*}

A submersion is locally a projection, i.e. around any $e\in E$ there is a neighbourhood diffeo to some $E'\times B'$, such that $\pi$ is just a projection map to $B'\subseteq B$ in these co-ordinates. This reduces to the case where $\pi$ is a projection, which is easy.