Example

• ((a → b) ∧ a) → b

1	Assume (a → b) ∧ a			Assume we have z :: (a -> b, a)
2	From (1), conclude a → b	(∧E)		fst z	:: a -> b
3	From (1), conclude a	(∧E)		snd z	:: a
4	From (3) and (2), conclude b	(→E)		(fst z (snd z))	:: b
5	From (1) and (4), conclude ((a → b) ∧ a) → b	(→I)	(disch. 1)	\z -> (fst z (snd z))	:: (a -> b, a) -> b