Prove $(B \implies (C \implies D)) \implies (C \implies (B \implies D))$ without the Deduction Theorem

Question

I am reading "Introduction to Mathematical Logic" by Elliott Mendelson, and I am currently at the axiomization of propositional calculus. Mendelson presents the following three axioms (with modus ponens as the only rule of inference):

$A1: B \implies (C \implies B)$

$A2: (B \implies (C \implies D)) \implies ((B \implies C) \implies (B \implies D))$

$A3: (\lnot C \implies \lnot B) \implies ((\lnot C \implies B) \implies C)$

Immediately after this, Mendelson proves $B \implies B$ and then leaves it as an exercise to prove $(\lnot C \implies \lnot B) \implies (B \implies C)$. Mauro provided a great and detailed proof of the latter in response to the following post: Prove $( \lnot C \implies \lnot B) \implies (B \implies C)$ without the Deduction Theorem

He does so by using several intermediate results, namely:

$T1: (C \implies D) \implies ((B \implies C) \implies (B \implies D))$

$T2: (B \implies (C \implies D)) \implies (C \implies (B \implies D))$

My question is centered around the proof of T2. Mauro proves T2 by proving and then using another intermediate result:

$T3: B \implies ((B \implies C) \implies C)$

However, I believe I found a proof that doesn't require T3. I would like to know if my proof is correct or if there is something I'm missing. Here is my proof (using [ ] occasionally for readability):

$1. \; [B \implies (C \implies D)] \implies [(B \implies C) \implies (B \implies D)]$

—A2

$2. \; [(B \implies C) \implies (B \implies D)] \implies [(C \implies (B \implies C)) \implies (C \implies (B \implies D))]$

—T1

$3. \; [B \implies (C \implies D)] \implies [(C \implies (B \implies C)) \implies (C \implies (B \implies D))]$

—From 1, 2, T1, and MP twice

$4. \; [(B \implies (C \implies D)) \implies (C \implies (B \implies C))] \implies [(B \implies (C \implies D)) \implies (C \implies (B \implies D))]$

—From 3, A2, and MP

$5. \; (C \implies (B \implies C))$

—A1

$6. \; [(B \implies (C \implies D)) \implies (C \implies (B \implies C))]$

—From 5, A1, and MP

$7. \; [(B \implies (C \implies D)) \implies (C \implies (B \implies D))]$

—From 4, 6, and MP

Answer 1

Your proof is correct, but you don’t really need T1 either. It’s easiest, in my opinion, to just prove Hypothetical Syllogism as a meta-theorem, and then proceed.

If you’re unfamiliar with the proof of said meta-theorem, here it is:

1. $A \to B~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~$[Premise]
2. $B \to C~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~$[Premise]
3. $(B \to C) \to (A \to (B \to C))~~~~$ [A1]
4. $(A \to (B \to C)) \to ((A \to B) \to (A \to C))~~~~~~~~~$ [A2]
5. $A \to (B \to C)~~~~~~~~~~~~~~~~~~~~~~~~~~~~$ [2,3 MP]
6. $(A \to B) \to (A \to C)~~~~~~~~~~~~~~~~~$[5,4 MP]
7. $A \to C~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~$[1,6 MP]

Then, we can proceed more naturally. I’m going to leave the citations undone since they’re just axioms, modus ponens, or Hypothetical Syllogism.

1. $(A \to (B \to C)) \to ((A \to B) \to (A \to C))$

2. $((A \to B) \to (A \to C)) \to (B \to ((A \to B) \to (A \to C)))$

3. $(A \to (B \to C)) \to (B \to ((A \to B) \to (A \to C)))$

4. $(B \to ((A \to B) \to (A \to C))) \to ((B \to (A \to B)) \to (B \to (A \to C)))$

5. $(A \to (B \to C)) \to ((B \to (A \to B)) \to (B \to (A \to C)))$

6. $5 \to ((A \to (B \to C)) \to (B \to (A \to B))) \to ((A \to (B \to C)) \to (B \to (A \to C)))$

7. $((A \to (B \to C)) \to (B \to (A \to B))) \to ((A \to (B \to C)) \to (B \to (A \to C)))$

8. $B \to (A \to B)$

9. $8 \to ((A \to (B \to C)) \to (B \to (A \to B)))$

10. $(A \to (B \to C)) \to (B \to (A \to B))$

11. $(A \to (B \to C)) \to (B \to (A \to C))$