Next  Types Are Theorems; Programs Are Proofs  12 
Write a proof
To prove a → b, assume a and present an argument for b (→I)
If a is proved, and if a → b is proved, then b is proved (→E)
For example, let's prove (a → b) → (b → c) → (a → c)
1  Assume a → b  
2  Assume b → c  
3  Assume a  
4  From (3) and (1), conclude b  (→E)
 
5  From (4) and (2), conclude c  (→E)
 
6  From (3) and (5), conclude a → c  (→I)  (discharges 3)

7  From (2) and (6), conclude (b → c) → (a → c)  (→I)  (discharges 2)

8  From (1) and (7), conclude (a → b) → (b → c) → (a → c)  (→I)  (discharges 1)

Could we stop at step 7 and conclude (b → c) → (a → c)?
No, because assumption 1 is still undischarged
Next  Next 