Example from Jan Łukasiewicz, Elements of Mathematical Logic (Pergamon Press, 1963), page 42.
Starting from your axiom (B3) $[(p \to q) \to ((q \to r) \to (p \to r))]$ with substitution: $[p \leftarrow (p \to q), q \leftarrow ((q \to r)\to(p \to r)), r \leftarrow s]$ we get:
$[((p \to q) \to ((q \to r)\to(p \to r))) \to ((((q \to r)\to(p \to r)) \to s) \to ((p \to q) \to s))]$
The antecedent is (B3) again; thus, by Modus Ponens, we get:
(T4) $(((q \to r)\to(p \to r)) \to s) \to ((p \to q) \to s)$.
In the same way (from (T4) and a suitable substitution) we get:
(T5) $[(p \to (q \to r))] \to ((s \to q) \to [p \to(s \to r)]).$
The basic "proof technique" is to identify a suitable substitution in some axiom or already proven thesis such that the result is a "big" conditional where the antecedent is an axiom or an already proven thesis and the consequent is the thesis to be proved.
We can see it in the derivation of $p \to p$ [page 45: your (1)].
From (B3) again, with substitution $[q \leftarrow (\lnot p \to q)]$ we get: $[p \to (\lnot p \to q)] \to [((\lnot p \to q) \to r) \to (p \to r)]$.
The antecedent is axiom (B2) and thus by MP we get (T9): $((\lnot p \to q) \to r) \to (p \to r)$ [that seems quite strange...].
Now, from (T9) with substitution $[q \leftarrow p, r \leftarrow p]$ we get: $((\lnot p \to p) \to p) \to (p \to p)$.
The antecedent is axiom is (B1); using MP we get: (T16) $p \to p$.
Going on, we have [page 45]: (T18) $q \to (p \to q)$ [which is (A1) of L1], and "the very important law of commutation" [page 47]: (T21) $(p \to (q \to r)) \to (q \to (p \to r))$.
Then [page 49]: (T35) $(p \to (q \to r)) \to [(p \to q) \to (p \to r)]$ [which is (A2) of L1].
Thesis 35 occurs as an axiom in the first axiom system of the sentential calculus, given by Frege in his Begriffsschrift.
The main difficulty in Łukasiewicz's original book is the lack of the $\text { Deduction Theorem}$.
Regarding axiom (A3) of L1, we can use "the very important law of double
negation" [page 50]:
(T39) $\lnot \lnot p \to p$ and (T40) $p \to \lnot \lnot p$,
as well as "the four laws of transposition" [page 51]:
(T46) $(p \to q) \to (\lnot q \to \lnot p)$, etc.
What we can do now is to use (T46): $(\lnot q \to p) \vdash (\lnot p \to \lnot \lnot q)$ with (T39) and your (2) above to get:
$(\lnot q \to p) \vdash (\lnot p \to q)$.
Using it with $(\lnot q \to \lnot p)$ and (2) again we get:
$(\lnot q \to \lnot p), (\lnot q \to p) \vdash (\lnot q \to q)$.
Finally, using axiom (B1) of L2 and MP we get:
$(\lnot q \to \lnot p), (\lnot q \to p) \vdash q$.
Best Answer
We have to use (A4) to "import" all the needed transformations:
Thus, using (A4), we have:
Consider now: $[(C \lor D) \lor (B \lor B)]$. By (A1) using (A4) we get:
We need also the Associativity Lemma:
Using 2) above and (b) again we get:
Now, the same approach must be used to derive:
Proof of Associativity:
Lemma 1: if $\vdash A \to C$ and $\vdash B \to C$, then $\vdash A \lor B \to C$.
$B \to C$
$(A \lor B) \to (C \lor A)$ --- from 1) and (A4) with (A3), by MP
$A \to C$
$(C \lor A) \to (C \lor C)$ --- as above
Lemma 2: if $\vdash A \to B$, then $A \to (C \lor B)$ and $A \to (B \lor C)$
$A \to B$
$A \to (B \lor C)$ --- from 1) and (A2) using (b)
$A \lor (C \lor B)$ --- from 2) and (A3).
Lemma:
$A \to [A \lor (B \lor C)]$ --- (A2)
$B \to (B \lor C)$ --- (A2)
$B \to [A \lor (B \lor C)]$ --- from 2) by Lemma 2
$(A \lor B) \to [A \lor (B \lor C)]$ --- from 1) and 3) by Lemma 1
$C \to [A \lor (B \lor C)]$ --- from $\vdash C \to C$ [your (d)] and Lemma 2 twice.