There are two inference rule of propositional logic involving implication (which I write using $\to$ instead of $\Rightarrow$):

The *introduction* rule says that we can prove $A \to B$ if we derive $B$ from the assumption $A$ (there are brackets around $[A]$ because $A$ here is a "temporary" assumption which is "discharged" by $A \to B$):
$$\frac{\begin{matrix}[A]\\ \vdots \\ B\\\end{matrix}}{A \to B}$$

The *elimination* rule says that from $A \to B$ and $A$ we may derive $B$:
$$\frac{A \to B\qquad A}{B}$$

Now consider what happens if we prove $A \to B$ in the elimination rule using the introduction rule. We get a derivation that looks like this:
$$\frac{\displaystyle
\frac{\begin{matrix}[A]\\ \vdots \\ B\\\end{matrix}}{A \to B} \qquad
\frac{\begin{matrix} \\ \\ \vdots \\\end{matrix}}{A}
}{B}$$
In words this proof would go as follows:

- Show that $B$ follows from the assumption $A$, thereby conclude $A \to B$.
- Prove $A$.
- Combine the previous two steps to conclude $B$.

We can transform the proof into a simpler one: step one already contains the proof of $B$, except that it relies on the assumption $A$. But we can get rid of the assumption by replacing it with the proof of $A$ whenever it gets used. So our new proof will look like this:
$$
\begin{matrix}\vdots \\ A\\ \vdots \\ B\\\end{matrix}
$$
This is what is meant by proof *simpliication*. It is a transformation of a proof in which an introduction rule is immediately followed by an elimination rule. Another example is this:
$$\frac{\displaystyle
\frac{A \qquad B}{A \land B}
}
{A}
$$
There is no point in first proving $A \land B$ and then forgetting about the proof of $B$ – we can just directly go for the upper-left part, which is a proof of $A$.

These proof transformations correspond precisely to computation steps in a functional programming language. The first example is the $\beta$-rule
$$(\lambda x : A \,.\, e_1) \, e_2 \leadsto e_1[e_2/x]$$
which reads: "a function mapping $x$ of type $A$ to an expression $e_1$ of type $B$ applied to an expression $e_2$ of type $A$ equals the expression $e_1$ with $x$ replaced by $e_2$". By the Curry-Howard correspondence $x$ is the assumption $A$, $e_1$ is the proof that $B$ follows from $A$, $\lambda x : A \,.\, e_1$ is the proof of the implication $A \to B$, $e_2$ is the proof of $A$, and $e_1[e_2/x]$ is the "simplified" (logicians say "reduced" or "normalized") proof of $B$ in which the assumption $x$ was replaced by $e_2$.

The second example corresponds to the rule for computng the first component of a pair:
$$\pi_1 \langle e_1, e_2 \rangle \leadsto e_1.$$