Is there a name for the propositional tautology (and it's associated rule) $Q\Rightarrow(P\Rightarrow Q)$? I have the tautology $Q\Rightarrow(P\Rightarrow Q)$. I can prove this intuitionistically:
Rule 
  Conclusion
    Q=>(P=>Q)
  Proof
    Suppose
      Q
    Hence
      Suppose
        P
      Hence
        Q
      P=>Q
    Q=>(P=>Q)

This gives the corresponding inference rule:
$$
\frac{Q}{P\Rightarrow Q}\quad\text{[VacuousImplicationIntroduction]}
$$
The proof, which relies on the tautology, is:
Rule (VacuousImplicationIntroduction)
  Premise
    Q
  Conclusion
    P=>Q
  Proof
    Q=>(P=>Q)
    Q
    P=>Q by ModusPonens

I've called this rule 'vacuous implication introduction', which is a pretty poor name. Is there a standard or at least a better one?
 A: Different authors have called the formula (not the rule) different names.
I've seen 'positive paradox', 'simplification', and 'Simp'.
I prefer to call the formula [p => (q => p)] or CpCqp in Polish notation, recursive variable prefixing.  Why?  Because under the the rule of detachment (also called modus ponens) it allows you to prefix any formula with a variable.  And since you can do that for any formula, you can recursively prefix each new formula with a variable in a proof sequence with prefixed formulas.  Or perhaps better, it allows to demonstrate metalogically that where 't' indicates a theorem or an axiom, that
$\vdash$Ca$_1$Ca$_2$...Ca$_n$t
CpCqp may look dull, but taking it as the only axiom under the rule of condensed detachment, which I'll call {CpCqp}, any theorem t which replaces CpCqp as the sole axiom has the same consequences as {CpCqp}.  
In other words, where $\vdash$t in {CpCqp}, 
{t} |-| {CpCqp}  
where |-| indicates deductive equivalence.
Not many non-trivial systems have that sort of property. 
