Example

• This one is sufficiently complicated that it's not obvious:

       ((a ∨ (a → b)) → b) → b 

1	Assume (a ∨ (a → b)) → b)
2	Assume a
3	From (2), conclude a ∨ (a → b)	(∨I)
4	From (3) and (1), conclude b	(→E)
5	From (2) and (4), conclude a → b	(→I)	(discharge 2)
6	From (5) conclude a ∨ (a → b)	(∨I)
7	From (6) and (1), conclude b	(→E)
8	From (1) and (7), conclude (a ∨ (a → b)) → b) → b	(→I)	(discharge 1)