My reference is "A Course on Mathematical Logic" by S.M. Srivastava.
This question is about a certain inference rule for proofs in first order logic. If $L$ is a first order language and $T$ is a theory written in $L$, you define a proof in $T$ to be a finite string of formulas $A_1,\dots,A_n$ such that each of the $A_i$ is either a logical axiom (like $\neg A\vee A$ for any forumla $A$), a non-logical axiom (a formula of $T$, an 'axiom' of $T$) or obtained from one or more of the $A_1,\dots,A_{i-1}$ by one of the rules of inference listed in the book. One such rule is the 'intuitive' expansion rule which states that if you've written down $A$ in your proof, and $B$ is any formula you like, you are allowed to write down $B\vee A$.
There is one such rule that I don't quite understand, the $\exists$-introduction rule : if you have already written down $A\rightarrow B$, and $x$ is a variable that is not free in $B$, then you can write down $\exists x A\rightarrow B$.
There is a little ambiguity, but I believe what is meant is $(\exists x A)\rightarrow B$.
What is the meaning of this? Can it be motivated by concrete examples? Why is it 'true'?