Validate Hilbert-style proof of $A \to (B\to C), B \vdash A \to B$

Question

Was hoping to get my proof of $A \to (B\to C), B \vdash A \to B$ checked to see if it makes sense, as I only ended up using one of the premises:

(1) $B$ (premise)

(2) $B \equiv \top $ (1 with Metatheorem $B \vdash B \equiv T$)

(3) $\neg A \vee B \equiv \neg A \vee \top $ (2 with Leibniz; $\neg A \vee p$)

(4) $\neg A \vee B$ (3 + Theorem $\vdash \neg A \vee \top$ with Equanimity)

(5) $A \to B$ (4 with Theorem $\vdash A \to B \equiv \neg A \vee B$)

Answer 1

It's hard to keep track of all the rules and metatheorems you're using (these things vary widely from treatment to treatment). But every step you do here seems plausible. In particular, the fact that you only used one premise is okay... we do in fact have $B\vdash A\to B,$ so the first premise is irrelevant.

However, I would expect a simpler proof, something along the lines of

1. $B$ (Premise)
2. $B\to (A\to B)$ (Usually an axiom instance in Hilbert style systems).
3. $A\to B$ (1,2,MP)