Explanation of implication-introduction rule
Every assumption that is introduced between brackets has to be discharged at some point for the proof to be complete. Otherwise, we could prove that $A$ is true for any given $A$ as follows.

[A]¹
───
 A


This proof is incorrect, we have not discharged the initial assumption. The following proof of $A\to A$ would be correct, as it discharges the assumption (and the implication introduction rule is necessary to do so!).

 [A]¹
 ───
  A
───── (discharging ¹)
A → A


Now, let's compare two derivations of $A \to A \times A$ and $A \to A \to A \times A$. On the first one, we will discharge the two occurrences of $A$ at the same time (on the same deduction step). On the second one, we will discharge the two occurrences on two separate steps.

First proof

  [A]¹   [A]²        
  ─────────   
    A × A        
───────────── (discharging ¹ and ²)
  A → A × A   


Second proof

 [A]¹    [A]²             
 ──────────          
   A × A             
───────────── (discharging ¹, note that ² is still alive!)   
  A → A × A        
──────────────── (discharging ²)
 A → A → A × A


Maybe looking at this from the perspective of the simply-typed lambda calculus is more illuminating. Instead of tracking superscripts, variable
names represent which assumptions are we choosing to discard at each point. Note the difference between the two proofs, and how the introduction rule of the implication corresponds to a lambda abstraction, 
while the introduction rule of the conjunction corresponds to a pair type.

First proof

   a : A   a : A        
   ─────────────     
   (a,a) : A × A        
 ────────────────────
 λa.(a,a) : A → A × A


Second proof

     a : A   b : A             
     ─────────────          
     (a,b) : A × A             
   ────────────────────     
   λb.(a,b) : A → A × A        
 ───────────────────────────
 λa.λb.(a,b) : A → A → A × A 


(I am using a lambda interpreter I wrote to generate these derivation trees. It may be useful for you if you are interested in the connection between propositional intuitionistic logic and lambda calculus.)