Deductive proof with Hilbert system

Question

Given b→a, and⌝(a→⌝b)

I'm trying to derive b. Obviously I can use some identities (like De Morgan) to show that ⌝(a→⌝b) is equivalent a∧b. However, I'd like to avoid using any other connectives than → and⌝, and rather prove using rules like Contrapositive, Transitivity, Double negation, Modus Ponens, etc (those of Hilbert system).

I struggled to prove this, but couldn't, as easy as it may seem. I'd appreciate your help please.

Answer 1

Use Mendelson's First Axiom :

1) $\lnot b \to (a \to \lnot b)$.

Use the same axiom to derive, by Modus Ponens, from 2nd premise :

2) $\lnot b \to \lnot (a \to \lnot b)$.

Use 1) and 2) and Mendelson's Third Axiom to derive, by Modus Ponens :

$b$.

Answer 2

$$ \neg (a \rightarrow \neg b) \iff \neg(\neg a \vee\neg b) \iff \neg\neg a \wedge \neg\neg b \iff a\wedge b $$