[Haskell-cafe] Propositional logic question

[Dave Tapley]

Hopefully this is just about on topic enough..
(Oh and it's not home work, I just can't bring myself to let it go!)

Taken from "Simon Thompson: Type Theory and Functional Programming"

Section 1.1
Exercise 1.3

Question: Give a proof of (A => (B => C)) => ((A /\ B) => C).

Now I can easily perform (and verify, it's given earlier in the
section) the proof of implication with the terms flipped around:
((A /\ B) => C) => (A => (B => C))
Thus:

[A]2  [B]1
----------- (/\ I)      [(A /\ B) => C]3
  A /\ B
---------------------------------------- (=> E)
                   C
                 --------- (=> I) 1
                 B => C
                 ------------------ (=> I) 2
                 A => (B => C)
                 --------------------------- (=> I) 3
                 ((A /\ B) => C) => (A => (B => C))


My problem arrives finding a solution to the exercise question, my
approach is to basically run the above proof backwards.
Thus:

A => (B => C)     A
--------------------- (=> E)     B
      B => C
--------------------- (=> E)
           C

Now at this point I thought "aha, I can use (=> I) to introduce (A /\
B)" and get:

--------------------- (=> I) 1
    (A /\ B) => C

But here I am only entitled to discharge (A /\ B) in the preceding
proof and not A and B on their own.
What proof which would allow me to discharge my assumptions A and B?

I can see in my head how it makes perfect sense, but can't jiggle a
way to do it using only the given derivations.

Many thanks,
Dave