Deriving $A \rightarrow ( B \rightarrow C ) \rightarrow ( ( A \rightarrow B ) \rightarrow ( A \rightarrow C ) )$ in the sequent calculus I need to prove the following theorem:
$A\to (B\to C) \to ((A\to B) \to (A\to C))$  
using the sequent calculus method.
Using the rules: 
$$ G, A \Rightarrow B,D  \over  G \Rightarrow A \to B , D $$ 
and 
$$ G \Rightarrow A,D  \ \ \ \  G,B \Rightarrow D  \over A\to B \Rightarrow D $$  
and the Identity Axiom :
$$ \over G,A \Rightarrow A,D $$    


*

*$\to$ is an ordinary implication sign,

*$\Rightarrow$ is the sequential implication sign,

*$G,D$ are finite (and possibly empty) sets of propositions, and 

*$G\Rightarrow D$ is to mean, that the conjuction of the propositions in $G$, implies the disjunction of those in $D$. 


I really can't go anywhere so far, thanks for your help in advance.
 A: Sequent proofs should tend to write themselves without you having to think about them (which is the the point of using them!). The motto is: start from where you want to end up and work backwards (or rather upwards: in other words, write the sequent you want to prove at the bottom, and construct the tree from bottom to top ...).
You want to establish the sequent

$$\Rightarrow A\to (B\to C) \to ((A\to B) \to (A\to C))$$

Given your rules, that can only come from 

$$A\to (B\to C) \Rightarrow  (A\to B) \to (A\to C)$$

which in turn must surely come from

$$A\to (B\to C), (A\to B) \Rightarrow  A\to C$$

which in turn must come from

$$A\to (B\to C), (A\to B), A \Rightarrow C$$

So how do we get that? We'll have to use your final rule. Deal with the most complex wff first, and that must come from 
$$(B\to C), (A \to B), A \Rightarrow C\quad   and\quad  A\to B, A \Rightarrow A, C$$
You can see how to get the right-hand one of those (it's what you are calling an identity)! So what about the left sequent? That comes from e.g. 

$$C, (A \to B), A \Rightarrow C \quad and\quad (A \to B), A \Rightarrow B, C$$

And you can immediately see how to get the left-hand one of those. And the right-hand sequent obviously comes from

$$B, A \Rightarrow B, C \quad and \quad A \Rightarrow A, B, C$$

Turn all that the other way up to get a top-to-bottom proof from "identities" (better "axioms") via the rules for moving $\to$ around.
The moral is you don't have to puzzle to construct this sort of proof. To repeat: just write your proof "from the bottom up" doing the obvious thing at every stage. That, as I said, is the delight of sequent proofs!
A: What you've called "rule" is usually called "axiom" or "axiom scheme" and "identities" are usually called "rules".


*

*$A \Rightarrow A, B, C$ (axiom) and $A, B \Rightarrow B, C$ (axiom) implies $A, A\rightarrow B \Rightarrow B, C$  by the second rule.

*1 and $A, A\rightarrow B, C \Rightarrow C$ (axiom) implies $A, A\rightarrow B, B\rightarrow C \Rightarrow C$ by the second rule.

*$A \rightarrow B,A \Rightarrow A, C$ (axiom) and 2 implies $A, A\rightarrow B, A\rightarrow(B\rightarrow C) \Rightarrow C$ by the second rule.

*3 implies $A\rightarrow B, A \rightarrow(B\rightarrow C) \Rightarrow A\rightarrow C$ by the first rule.

*4 implies $A \rightarrow(B\rightarrow C) \Rightarrow (A\rightarrow B )\rightarrow(A\rightarrow C)$ by the first rule.

*5 implies $\Rightarrow (A \rightarrow(B\rightarrow C)) \rightarrow ((A\rightarrow B )\rightarrow(A\rightarrow C))$ by the first rule.
A: A "long" comment.
You can use this example to "format" the sequent calculus axiom and rules :

$${  \quad \over \Gamma, A \implies A, \Delta } \, \text{(Axiom)}$$
$${ \Gamma \implies A \quad B \implies \Delta \over \Gamma \implies A \rightarrow B, \Delta } \, \text{(Rule)}$$

