What is this property relating to logical systems called? 
See the revised version of this question here.

The following property exhibited by some logical systems has captured my attention:
$$x_1 \vdash x_2    \text{ if and only if }  \vdash (x_1 \rightarrow x_2)$$
for any well-formed formulas $x_1$ and $x_2$.
My question is 3-fold:  


*

*Does this property have a name? If so, what is it called?

*Does classical propositional logic have this property? (I'm assuming it does, but I want to be sure.) What other systems display this property? 

*Does the presence of this property (or lack thereof) imply any other important properties about the system in question? (I realize that this third part of the question might seem overly broad, but what I really want to know is: is this property important and if so, why? Deep insights appreciated.)


EDIT: Apparently my notation for "provability" was non-standard and throwing people off (folks thought I was describing the deduction theorem), so I corrected it. Thanks @Hurkyl. 
EDIT #2: Based on guidance from this meta question, I've reverted my corrections back to the original (wrong) notation so as not to invalidate the answers I've already received here. The revised version of this question with the necessary notational (and semantic) changes has nothing to do with the deduction theorem, as far as I know.
 A: This is called the deduction-resolution property; it's probably best to think of it as $$\Gamma,\alpha \vdash \beta \iff \Gamma \vdash \alpha \rightarrow \beta.$$
Under the usual way of thinking about things, first-order logic does have this property, but we assume that $\alpha$ is a sentence, not just a formula.
It's worth noting the close relationship to the lattice-theoretic perspective on implication, in which the formula $$a \wedge b \leq c \iff a \leq b \rightarrow c$$ defines logical implication, also known as "relative pseudocomplements", also known as "exponential objects." See here, for example.
Note also the connection to Cartesian closed categories, closed monoidal categories, and closed multicategories. The latter categorify the deduction-resolution property to give a notion of internal homs with possibly-multiple arguments.
A: This is called the deduction theorem. Yes, it holds in classical propositional logic and it does hold in classical logic, provided that either you restrict it to conditionals with closed antecedents (thus blocking the problematic inference involving a formula with free variables in the antecedent) or you restrict the universal generalization rule (Jeffrey Ketland has some interesting remarks on the options in this blog post; check out the article linked in his post).  
A: You can call it the deduction theorem, though sometimes only the first half of the 'if and only if' gets called the deduction theorem.  
Yes, classical propositional logical has this property.  In Polish notation, the if part follows from the axioms CpCqp and CCpCqrCCpqCpr ('C' is the conditional), and many other sets of axioms.  It holds for any natural deduction system as well as any system that has a rule of uniform substitution, a rule of detachment, and has as axioms or theorems CpCqp and CCpCqrCCpqCpr (or their isomorphic equivalents in other notational schematics).
Yes, the presence of that property implies some other important properties... or maybe better important denials of properties.  It implies that the system is not a relevant logic, because no relevant logic has CpCqp (or an isomorphic equivalent) as a theorem.  Also, and I'm just figuring this out...
The property you've mentioned implies that Cpp is a theorem.  Now, assume that the operator 'C' associates.  But, CpCqp is a theorem.  So, CpCpp is a theorem.  If associativity holds and the system is sound and complete, then CCppp is a theorem also.  Since Cpp is a theorem, by detachment 'p' will then also hold.  Thus, if such a system is sound and complete, associativity will fail, since no system (with at least two truth values) is sound if 'p' is a theorem since 'p' could mean falsity.
Or in other words, the presence of soundness and completness for the system along with that property implies that the implication operator will NOT be associative.  And thus the algebraic structure of such a system cannot be that of a group or semigroup.
