Hilbert's sequent calculus axiom:
(1.1)$A\supset (B\supset A)$
(1.2)$(A\supset (B\supset C))\supset((A\supset B)\supset (A\supset C))$
(2.1)$A\supset (A\vee B)$
(2.2)$B\supset (A\vee B)$
(2.3)$(A\supset C)\supset((B\supset C)\supset ((A\vee B) \supset C))$
(3.1)$(A\wedge B) \supset A$
(3.2)$(A\wedge B) \supset B$
(3.3)$(C\supset A)\supset((C\supset B)\supset (C \supset (A\wedge B))$
(4.1)$(A\supset B)\supset((A\supset \neg B)\supset \neg A)$
(4.2)$A\supset (\neg A \supset B)$
(4.3)$A\vee \neg A$
and there is a rule "Modus Ponens".
If $A$ and $A\supset B$ is either a formal theorem, then $B$ is also a formal theorem.
I am puzzling with proving (Question).
(Question)$(A\supset B)\supset((C\supset A)\supset (C\supset B))$
How prove (Question)?
Using Hilbert-style calculus with modus ponens (no sequent calculus) and without Deduction Theorem, we have :
Ax 1.1) $P \supset (Q \supset P)$
Ax 1.2) $(P \supset (Q \supset R)) \supset ((P \supset Q) \supset (P \supset R))$
Now the deduction :
1) $(A \supset B) \supset (C \supset (A \supset B))$
is an instance of Ax 1.1, with $P := (A \supset B)$ and $Q := C$
2) $(C \supset (A \supset B)) \supset ((C \supset A) \supset (C \supset B))$
is an instance of Ax 1.2, with $C$ in place of $P$, $A$ in place of $Q$ and $B$ in place of $R$
Let $X := (C \supset (A \supset B))$ and let $Y := ((C \supset A) \supset (C \supset B))$ , so that 2) is : $(X \supset Y)$
3) $(X \supset Y) \supset ((A \supset B) \supset (X \supset Y))$
is an instance of Ax 1.1 with $(X \supset Y)$ in place of $P$ and $(A \supset B)$ in place of $Q$
4) $((A \supset B) \supset (X \supset Y))$
by 2), 3) and MP
5) $((A \supset B) \supset (X \supset Y)) \supset ((A \supset B) \supset X) \supset ((A \supset B) \supset Y)$
is a (very complicated) instance of Ax 1.2 with $(A \supset B)$ in place of $P$, $X$ i.e. $(C \supset (A \supset B))$, in place of $Q$ and $Y$ i.e. $((C \supset A) \supset (C \supset B))$ in place of $R$
6) $(A \supset B) \supset Y$
i.e.
$(A \supset B) \supset ((C \supset A) \supset (C \supset B))$
from 5, 4 and 1 with MP twice.
If we have the Deduction Theorem, the proof is much simpler :
a) assume $(A \supset B)$
b) $(A \supset B) \supset (C \supset (A \supset B))$ --- as above : is an instance of Ax 1.1
c) $(C \supset (A \supset B))$ --- from a) and b) by MP
d) $(C \supset (A \supset B)) \supset ((C \supset A) \supset (C \supset B))$ --- as above : is an instance of Ax 1.2
e) $((C \supset A) \supset (C \supset B))$ --- from c) and d) by MP
In this way we have :
$(A \supset B) \vdash ((C \supset A) \supset (C \supset B))$
Now we can apply the Deduction Theorem and get :
f) $\vdash ( (A \supset B) \supset ((C \supset A) \supset (C \supset B)) )$.