Let's try an example. Let's say you're trying to prove the following:
Simple Theorem over the natural numbers: If $n$ is even, then $n+1$ is odd.
What he's trying to say is that you don't need an independent proof that $n$ is even. In the natural numbers, this isn't even true, since not all numbers are even. What he's trying to say is that when trying to prove an implication like the Simple Theorem above, you're allowed to introduce the assumption that $n$ is even, and from that assumption, together with whatever other axioms you're using, try to prove that $n+1$ is odd. If you succeed in this, you can now correctly conclude that the implication is true.
From his paper:
The rule makes intuitive sense, a proof justifying A ⊃ B true assumes, hypothetically, the left-hand side of the implication so that A true, and uses this to show the right-hand side of the implication by proving B true. The proof of A⊃B true constructs a proof of B true from the additional assumption that A true.
The whole painful stuff with the bars and labels is a variation of the pain that comes with other deduction systems when you're trying to create a proof context to hold the introduction of an assumption. When these contexts get nested in a complicated proof, it requires machinery analogous to lexical variable scoping rules in programming languages. The assumptions have to come and go properly so they don't allow unsound deductions in other parts of the proof.
EDIT: per request of original poster.
OK, let's dig into this some more. I'm going to use some different notation. The notation
$$
\Gamma \vdash \sigma
$$
means some set of axioms $\Gamma$ proves some formula $\sigma$, where the turnstile $\vdash$ means "proves". Now the inference rule we're looking at can be written like this. We can conclude
$$
\Gamma \vdash A \rightarrow B
$$
if we can prove
$$
\{\Gamma; A\} \vdash B
$$
where the semicolon means we've added formula $A$ to the set of axioms $\Gamma$. Note that this also creates what I've been calling a "proof context" where we're keeping track of assumptions we've been making. The Pfenning paper uses labels on bars to do the same thing.
Let's try it on a complicated example with nested proof contexts: prove the tautology
$$
A \rightarrow (B \rightarrow (C \rightarrow B))
$$
In our notation, proving this tautology looks like this:
$$
\{\} \vdash A \rightarrow (B \rightarrow (C \rightarrow B))
$$
That is, $\Gamma$ is empty since we're proving a tautology.
Here we go, using our rule of inference.
We can prove
$$
\{\} \vdash A \rightarrow (B \rightarrow (C \rightarrow B))
$$
if we can prove
$$
\{A\} \vdash B \rightarrow (C \rightarrow B)
$$
Let's keep going.
We can in turn prove
$$
\{A\} \vdash B \rightarrow (C \rightarrow B)
$$
if we can prove
$$
\{A, B\} \vdash (C \rightarrow B)
$$
One more application of our rule:
We can prove
$$
\{A, B\} \vdash (C \rightarrow B)
$$
if we can prove
$$
\{A, B, C\} \vdash B
$$
But this follows easily: since B is already an axiom, it follows that we can prove it. But we only got this axiom from our inference rule that allowed us to add it safely.
