A two-premise formal deduction

The annotated derivation is: line $0$: $A$ (assumption); line $1$: $A\to (P(x)\to Q(x))$ (universal instantiation); line $2$: $P(x)\to Q(x)$ (MP on $0,1$); line $3$: $B$ (assumption); line $4$: $B\to P(x)$ (universal instantiation); line $5$: $P(x)$ (MP on $3,4$); line $6$: $Q(x)$ (MP on $5,2$); line $7$: $\mathrm{\forall }xQ(x)=C$ (generalization). Both substitutions are $x\mathrm{/}x$, which is free-for, and both assumptions are sentences, so generalization has no free-assumption obstruction.

Apply F1 to that eight-line proof to obtain $\{A\}⊢B\to C$ and, discharging $A$ instead, $\{B\}⊢A\to C$. Discharge the remaining sentence in the first proof to obtain $⊢A\to (B\to C)$. Thus the example displays a derivation and its actual discharged conclusions.