Fiber Product is an embedded submanifold 
Let $\pi:E\to B$ a smooth submersion and $\phi:F\to B$ a smooth map. Defining the fiber product of $E$ and $F$ with respect to $B$ as the set:
$$E\times_B F:=\{(e,f)\in E\times F\mid \pi(e)=\phi(f)\}$$
Prove that $E\times_B F$ is an embedded submanifold of $E\times F$.

I'm trying to find charts $\psi:U\cap (E\times_B F)\to\mathbb{R}^k$ where $U\subset E\times F$ is open, but I'm stuck since I don't even know where to look for the right $k$, which makes me think there is probably a simpler solution.
Any suggestions?
 A: 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: 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.
