Prove: $(A\rightarrow B),(A\rightarrow C)\rightarrow B, \mapsto_{HPC} B $

Question

I'd really like your help proving:

$(A\rightarrow B),(A\rightarrow C)\rightarrow B, \mapsto_{HPC} B $

Where $HPC$ is the Hilbert's system proof which contains the following relevant axioms:

1. $A\rightarrow(B \rightarrow A)$
2. $(A\rightarrow(B\rightarrow C)) \to ((A\rightarrow B)\rightarrow(A\rightarrow C))$
3. $(A\rightarrow B)\rightarrow ((A\rightarrow\bar{B})\rightarrow \bar{A})$
4. $\bar{\bar{A}} \rightarrow A$

In addition tried to use these following lemmas: $\bar{A} \rightarrow (A \rightarrow C) $ and $(A\rightarrow B)\rightarrow (\bar{B} \rightarrow \bar{A})$.

Any suggestions?

Answer 1

1. $A→B$ (premise)
2. $(A→C)→B$ (premise)
3. $(A→B)→(\neg B→\neg A)$ (your second lemma)
4. $\neg B→ \neg A$ (3,1)
5. $\neg A →(A→C)$ (your first lemma)
6. $(\neg A →(A→C))→(\neg B → (\neg A →(A→C)))$ (axiom 1)
7. $\neg B → (\neg A →(A→C))$ (6,5)
8. $(\neg B → (\neg A →(A→C))) → ((\neg B → \neg A)→(\neg B → (A→C)))$ (axiom 2)
9. $((\neg B → \neg A)→(\neg B → (A→C)))$ (8,7)
10. $\neg B → (A→C)$ (9,4)
11. $((A→C)→B)→(\neg B → \neg(A→C))$ (your second lemma)
12. $\neg B → \neg(A→C)$ (11, 2)
13. $(\neg B → (A→C))→((\neg B → \neg(A→C))→\neg \neg B)$ (axiom 3)
14. $(\neg B → \neg(A→C))→\neg \neg B$ (13, 10)
15. $\neg \neg B$ (14, 12)
16. $\neg \neg B → B$ (axiom 4)
17. $B$ (16, 15)