Some Preliminaries
First: before answering the question, it will be useful to rename the axioms and adopt some conventions that will also sneak something (yet to be named) in to resolve this question and others like it:
$$\begin{array}{ll}
I:& a ⊃ a,\\
K:& a ⊃ b ⊃ a,\\
S:& (a ⊃ b ⊃ c) ⊃ (a ⊃ b) ⊃ a ⊃ c,\\
Z:& (¬a ⊃ ¬b) ⊃ b ⊃ a,\\
A:& a ⊃ b ⊃ a∧b,\\
π_0:& a∧b ⊃ a,\\
π_1:& a∧b ⊃ b,\\
σ_0:& a ⊃ a∨b,\\
σ_1:& b ⊃ a∨b,\\
O:& (a ⊃ c) ⊃ (b ⊃ c) ⊃ a∨b ⊃ c.
\end{array}$$
Second: in here, and below, use $⊃$ for the conditional operator and adopt the conventions that it associates to the right, e.g. $a ⊃ b ⊃ c = a ⊃ (b ⊃ c)$ and that it binds more loosely than the other connectives, with $¬$ binding the strongest of all the connectives. For concreteness, we will write $f: a$ to state that $f$ is a proof of $a$. For modus ponens, if $f: a ⊃ b$ and $g: a$, then we write $fg: b$. Products associate to the left, e.g. $fgh = (fg)h$.
We can also define the following:
$$
\left(\begin{matrix}x: a\\y: b\end{matrix}\right) → (x, y) ≡ A x y: a ∧ b,\\
\left(\begin{matrix}f: a ⊃ c\\g: b ⊃ c\end{matrix}\right) → [f, g] ≡ O f g: a ∨ b ⊃ c.
$$
Third: some key lemmas may then be established and written succinctly as follows:
$$\begin{array}{rll}
I &= S K K:& a ⊃ a,\\
B &= S (K S) K:& (b ⊃ c) ⊃ (a ⊃ b) ⊃ a ⊃ c,\\
C &= S (B B S) (K K):& (a ⊃ b ⊃ c) ⊃ b ⊃ a ⊃ c,\\
W &= S S (K I):& (a ⊃ a ⊃ b) ⊃ a ⊃ b,\\
T &= B (S I) K:& a ⊃ (a ⊃ b) ⊃ b,\\
U &= S I:& ((a ⊃ b) ⊃ a) ⊃ (a ⊃ b) ⊃ b.
\end{array}$$
As an example and illustration, the proof is provided in line-by-line form for $T = B (S I) K$:
$$\begin{array}{ll}
B:& (e ⊃ d) ⊃ (a ⊃ e) ⊃ a ⊃ d,\\
S:& (c ⊃ a ⊃ b) ⊃ (c ⊃ a) ⊃ c ⊃ b,\\
I:& c ⊃ c,\\
S I:& (c ⊃ a) ⊃ c ⊃ b,\\
B (S I):& (a ⊃ e) ⊃ a ⊃ d,\\
K:& a ⊃ c ⊃ a,\\
B (S I) K:& a ⊃ d,
\end{array}$$
where the requirement that the modus ponens fits for $S I$, $B (S I)$ and $B (S I) K$ imposes the following constraints:
$$c = a ⊃ b,\quad e = c ⊃ a,\quad d = c ⊃ b,$$
so that the final result yields
$$T = B (S I) K: a ⊃ d = a ⊃ (a ⊃ b) ⊃ b.$$
Fourth: an equivalence relation between proofs can be defined, where $f = g$ may occur for two proofs $f$ and $g$ that yield the same results. For instance, if $x: a$, while we also have $I x: a$. If $f: a$ and $x: b$, then $K f x: a$. Finally, if $f: a ⊃ b ⊃ c$, $g: a ⊃ b$ and $x: a$, then $f x: b ⊃ c$, $g x: b$, so that $f x (g x): c$, while we also have $S f g x: c$.
Other relations may be imposed for $π_0$, $π_1$ and $A$: if $x: a$, $y: b$, then $(x,y): a ∧ b$, $π_0(x,y): a$, $π_1(x,y): b$. If $z: a ∧ b$, then $π_0 z: a$, $π_1 z: b$ and $(π_0 z, π_1 z): a ∧ b$.
On this basis we may assert the following proof equivalences:
$$
I x = x,\quad K f x = f,\quad S f g x = f x (g x),\\
π_0(x,y) = x,\quad π_1(x,y) = y,\quad (π_0 z, π_1 z) = z\quad (z: a ∧ b),
$$
the last one being constrained in its range of application.
Based on this, we have the following equivalence
$$
B f = S (K S) K f = K S f (K f) = S (K f),
$$
as well as the following, which may be derived similarly:
$$\begin{array}{rcl}
U g &=& S I g,\\
W f &=& S f I,\\
T g &=& S I (K g),\\
B f g &=& S (K f) g,\\
C f g &=& S f (K g).
\end{array}$$
With the inclusion of additional arguments, this can be further developed to the following:
$$
U g x = x (g x),\quad W f x = f x x,\quad T g x = x g,\quad B f g x = f (g x),\quad C f g x = f x g.
$$
It is actually possible to go even further and define
$$
\left(\begin{matrix}
f: b ⊃ c\\g: a ⊃ b
\end{matrix}\right) → f ∘ g ≡ B f g: a ⊃ c
$$
and assert additional equivalences such as
$$f ∘ I = f = I ∘ f,\quad (f ∘ g) ∘ h = f ∘ g ∘ h = f ∘ (g ∘ h).$$
The corresponding equivalence rule, as one might expect: $(f ∘ g) x = f (g x)$, which is just the rule for $B$. One consequence of this is that
$$f = f ∘ I = B f I = S (K f) I.$$
Fifth: what we need the most, here, is the Deduction Theorem, which states that given a proof $φ(x): b$ that depends on a stipulation $x: a$, there should exist a proof $λx·φ(x): a ⊃ b$, such that $λx·φ(x)$ is free of any occurrences of the stipulation/hypothetical $x$, such that $(λx·φ(x))x = φ(x)$. In fact, we can define it inductively over the structure of $φ(x)$ by:
$$
λx·x = I,\quad λx·a = K a,\quad λx·a x = a,\\
λx·u x = W a,\quad λx·u b = C a b,\quad λx·x b = T b,\\
λx·x v = U b,\quad λx·a v = B a b,\quad λx·u v = S a b,
$$
where $a$ and $b$ are free of any occurrences of $x$ in them, $u$ and $v$ each have at least one occurrence of $x$ in them, but with $u ≠ x ≠ v$, with $λx·u = a$, $λx·v = b$, such that $a x = u$, and $b x = v$.
Yes, I sneaked in the Curry-Howard-Lambek Correspondence.
The Deduction Theorem, in particular, corresponds to taking the "λ-abstractions", such as what was laid out above. There are other λ-abstraction algorithms, but this one will best suit our purposes.
We can go even further and work with structured stipulations/hypotheticals. For instance, if $x: a$ and $y: b$, with $φ(x,y): c$, then we may write
$$λ(x,y)·φ(x,y) ≡ λz·φ(π_0z,π_1z): a ∧ b ⊃ c.$$
In particular, we have the following equivalences
$$λ(x,y)·x = λz·π_0 z = π_0,\quad λ(x,y)·y = λz·π_1 z = π_1.$$
Finally, note that the term $x x$ cannot be made consistent with modus ponens, since this would require a proof of the form $x: (((⋯) ⊃ a) ⊃ a) ⊃ a$, yielding the proof $x x: a$. However, we could still add in $D = λx·x x$, just to round out the inductive construction of $λx·φ(x)$, and pretend it's well-defined, even though its proof would be $D: (((⋯) ⊃ a) ⊃ a) ⊃ a$. However, we're not going to need or use it anywhere.
Proof Of Distributivity I:
Now, with the preliminaries laid out, watch and see how fast the problem gets crunched.
First, to establish
$$Δ_0: a ∧ (b ∨ c) ⊃ (a ∧ b) ∨ (a ∧ c),$$
let
$$x: a,\quad y: b ∨ c,\quad v: b,\quad w: c.$$
Then
$$
(x,v): a ∧ b\quad→ σ_0(x,v): (a ∧ b) ∨ (a ∧ c)\quad→ υ_0 ≡ λv·σ_0(x,v): b ⊃ (a ∧ b) ∨ (a ∧ c),\\
(x,w): a ∧ c\quad→ σ_1(x,w): (a ∧ b) ∨ (a ∧ c)\quad→ υ_1 ≡ λw·σ_1(x,w): c ⊃ (a ∧ b) ∨ (a ∧ c).
$$
Therefore,
$$[υ_0,υ_1]: b ∨ c ⊃ (a ∧ b) ∨ (a ∧ c)\quad → [υ_0,υ_1] y: (a ∧ b) ∨ (a ∧ c).$$
Noting that $(x,y): a ∧ (b ∨ c)$, we have
$$Δ_0 ≡ λ(x,y)·[υ_0,υ_1] y: a ∧ (b ∨ c) ⊃ (a ∧ b) ∨ (a ∧ c).$$
This can be worked out in detail
$$
υ_0 = λv·σ_0(x,v) = λv·σ_0(A x v) = B σ_0 (A x),\\
υ_1 = λw·σ_1(x,w) = λw·σ_1(A x w) = B σ_1 (A x),\\
λ(x,y)·[υ_0, υ_1] y = λ(x,y)·O υ_0 υ_1 y = λz·O \bar υ_0 \bar υ_1 (π_1 z),
$$
where
$$
\bar υ_0 = B σ_0 (A (π_0 z)),\quad \bar υ_1 = B σ_1 (A (π_0 z)).
$$
Their respective λ-abstractions may then be worked out:
$$
\bar τ_0 = λz·\bar υ_0 = B (B σ_0) (B A π_0) = (B σ_0) ∘ A ∘ π_0,\\
\bar τ_1 = λz·\bar υ_1 = B (B σ_1) (B A π_0) = (B σ_1) ∘ A ∘ π_0.
$$
Therefore,
$$
λz·O \bar υ_0 \bar υ_1 (π_1 z) = S (λz·O \bar υ_0 \bar υ_1) π_1,\\
λz·O \bar υ_0 \bar υ_1 = S (λz·O \bar υ_0) \bar τ_1,\\
λz·O \bar υ_0 = B O \bar τ_0.\\
$$
Thus,
$$
Δ_0 = λz·O \bar υ_0 \bar υ_1 (π_1 z) = S (S (B O \bar τ_0) \bar τ_1) π_1.
$$
Expressed in pure $SK$ form, noting that $B O = S (K O)$, with other combinations of $B$ similarly eliminated:
$$
\bar τ_0 = S (K (S (K σ_0))) (S (K A) π_0),\\
\bar τ_1 = S (K (S (K σ_1))) (S (K A) π_0),\\
Δ_0 = S (S (S (K O) \bar τ_0) \bar τ_1) π_1.
$$
If written in line-by-line form, the $\bar τ$'s each use 9 axioms, and the overall term $Δ_0$ use 6 more axioms, for a total of 24 axioms, connected by 23 modus ponens, for a total of 47 lines.
You can write out the lines, if you wish, but there's no reason to (other than to check for errors and validate the result), since everything you need is already contained in this formula.
Proof Of Distributivity II:
For the converse, we want
$$Δ_1: (a ∧ b) ∨ (a ∧ c) ⊃ a ∧ (b ∨ c).$$
Let
$$w: a,\quad x: b,\quad y: c.$$
Then, noting that $(w,x): a ∧ b$ and $(w,y): a ∧ c$, we have
$$
σ_0x: b ∨ c ⇒ (w,σ_0x): a ∧ (b ∨ c) ⇒ λ(w,x)·(w,σ_0x): a ∧ b ⊃ a ∧ (b ∨ c),\\
σ_1y: b ∨ c ⇒ (w,σ_1y): a ∧ (b ∨ c) ⇒ λ(w,y)·(w,σ_1y): a ∧ c ⊃ a ∧ (b ∨ c).
$$
Thus
$$
Δ_1 = [λ(w,x)·(w,σ_0x), λ(w,y)·(w,σ_1y)]: (a ∧ b) ∨ (a ∧ c) ⊃ a ∧ (b ∨ c).
$$
Working this out in detail, we get
$$
(w,σ_0x) = Aw(σ_0 x) ⇒ λ(w,x).(w, σ_0 x) = λz·A (π_0 z) (σ_0 (π_1 z)) = S (B A π_0) (B σ_0 π_1),\\
(w,σ_1y) = Aw(σ_1 y) ⇒ λ(w,y).(w, σ_1 y) = λz·A (π_0 z) (σ_1 (π_1 z)) = S (B A π_0) (B σ_1 π_1).
$$
Thus
$$
Δ_1 = O (L_1 (B σ_0 π_1)) (L_1 (B σ_1 π_1))
$$
where
$$L_1 = S (B A π_0).$$
You can consolidate this, by noting that
$$L_1 (B φ π_1) = L_1 (C B π_1 φ) = B L_1 (C B π_1) φ = L_2 φ,$$
where
$$L_2 = B L_1 (C B π_1) = L_1 ∘ (C B π_1).$$
So, we can write
$$Δ_1 = O (L_2 σ_0) (L_2 σ_1) = [L_2 σ_0, L_2 σ_1],$$
where
$$L_2 = B (S (B A π_0)) (C B π_1) = (S (A ∘ π_0)) ∘ (C B π_1).$$
Reducing the $BC$ form to $SK$ form, we have:
$$L_2 = S (K (S (S (K A) π_0))) (S (S (K S) K) (K π_1)).$$
That's 14 axioms and 13 modus ponens for 27 lines.
Therefore, $Δ_1$ is 3 + 14 + 14 axioms, for a total of 31, and 30 modus ponens, for 61 lines.
The proofs are a lot smaller when you factor out the lemmas $L_1$ and $L_2$, and use $B$ and $C$.
More Examples - The Curry Rule And Its Inverse.
Consider next the Curry Rule and its inverse:
$$
⋀: (a ∧ b ⊃ c) ⊃ a ⊃ b ⊃ c,\quad ⋁: (a ⊃ b ⊃ c) ⊃ a ∧ b ⊃ c.
$$
For the Curry Rule, in cursory form, we have the following:
$$
f: a ∧ b ⊃ c,\quad x: a,\quad y: b,\\
(x,y): a ∧ b,\quad f (x,y): c,\\
λy·f(x,y): b ⊃ c,\quad λx·λy·f(x,y): a ⊃ b ⊃ c,\\
⋀ ≡ λf·λx·λy·f(x,y): (a ∧ b ⊃ c) ⊃ a ⊃ b ⊃ c.
$$
Worked out in detail,
$$
f(x,y) = f (A x y) = B f (A x) y = B (B f) A x y = C (B B B) A f x y,\\
⋀ = C (B B B) A.
$$
For the Inverse Curry Rule, we have the following development:
$$
g: a ⊃ b ⊃ c,\quad x: a,\quad y: b,\\
g x: b ⊃ c,\quad g x y: c,\quad (x,y): a ∧ b,\\
λ(x,y)·g x y = λz·g (π_0 z) (π_1 z): a ∧ b ⊃ c,\\
⋁ ≡ λg·λ(x,y)·g x y: (a ⊃ b ⊃ c) ⊃ a ∧ b ⊃ c
$$
When worked out in detail
$$g (π_0 z) (π_1 z) = B g π_0 z (π_1 z) = S (B g π_0) π_1 z$$
this leads to
$$
λz·S (B g π_0) π_1 z = S (B g π_0) π_1,\\
S (B g π_0) π_1 = S (C B π_0 g) π_1 = B S (C B π_0) g π_1 = C (B S (C B π_0)) π_1 g,\\
⋁ ≡ λg·S (B g π_0) π_1 = C (B S (C B π_0)) π_1
$$
Other Examples: Formulas With Negation
Proofs involving negation are more difficult. But, a few worthy of note are
$$V ≡ B Z K: ¬a ⊃ a ⊃ b,\quad N ≡ W (B Z V): ¬¬a ⊃ a,\quad N^{-1} ≡ Z N: a ⊃ ¬¬a.$$
Rules, such as $(¬a ⊃ a) ⊃ a$ or $(a ⊃ b) ⊃ ¬a ∨ b$, on the other hand, are harder to establish.
The name $N^{-1}$ isn't really justified, unless (or until) enough equivalence rules have been laid out for $Z$ to allow one to prove that $N ∘ Z N = I$ and that $Z (Z (Z N ∘ N)) = I$. The restricted form of the second identity is because $Z N ∘ N: ¬¬a ⊃ ¬¬a$ has a constraint on the propositions, which is undone by two applications of $Z$, while $N ∘ Z N: a ⊃ a$ is not constrained.
I don't know of any system of equational axioms that works with $Z$.
