Proving that the theorems of one logistic system are also theorems of another logistic system Question:
I am developing the proof for the following exercise from An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof by Peter B. Andrews:

X1102. Let $\mathscr{M}$ be the system which has the same wffs and rule of inference as $\mathscr{P}$, and the single axiom schema
$$\left[\mathbf{A} \supset \mathbf{B} \supset { }_\blacksquare \mathbf{C} \vee { }_\blacksquare \mathbf{D} \vee \mathbf{E} \right] \supset { }_\blacksquare \mathbf{D} \supset \mathbf{A} \supset { }_\blacksquare \mathbf{C} \vee { }_\blacksquare \mathbf{E} \vee \mathbf{A}$$
Show that each theorem of $\mathscr{P}$ is a theorem of $\mathscr{M}$.

Beginning of a Proof:
Start with a theorem $\mathbf{X}$ of $\mathscr{P}$. I want to prove that $\mathbf{X}$ is also a theorem of $\mathscr{M}$. To do so, look at the proof $\mathbf{X}_1 \ldots \mathbf{X}_n$ in $\mathscr{P}$ of $\mathbf{X}$ from the empty set. Consider $\mathbf{X}_i$ for some $i$ with $1 \leq n$. We need to prove by induction on $i$ that $\mathbf{X}_i$ has a proof in $\mathscr{M}$.
From the definition of a proof in $\mathscr{P}$, there are three cases to consider: (1) $\mathbf{X}_i$ is an axiom, (2) $\mathbf{X}_i$ is a member of the empty set, and (3) $\mathbf{X}_i$ inferred by modus ponens from $\mathbf{X}_j$ and $\mathbf{X}_k$ where $j < i$ and $k < i$. Condition (2) is never true for any $\mathbf{X}_i$ and (3) follows from a  trivial inductive argument.
Condition (1) is where I am struggling. Since $\mathscr{P}$ has three axiom schemata (see details below), I need to find a proof of each from the single axiom of $\mathscr{M}$. I'm not certain how to proceed from here. Am I even heading in the right direction? Should I look at proving any intermediary lemmas?
Definitions:
For clarification, here are the definitions with which I am working from the text. First, the syntactic and axiomatic structure of $\mathscr{P}$:

Definition. The set of wffs is the intersection of all sets $\mathscr{S}$ of formulas such that:
(i) $\mathbf{p} \in \mathscr{S}$ for each propositional variable $\mathbf{p}$.
(ii) For each formula $\mathbf{A}$ if $\mathbf{A} \in \mathscr{S}$, then $\mathord{\sim} \mathbf{A} \in \mathscr{S}$.
(iii) For all formulas $\mathbf{A}$ and $\mathscr{B}$, if $\mathbf{A} \in \mathscr{S}$ and $\mathbf{B} \in \mathscr{S}$, then $\left[\mathbf{A} \lor \mathbf{B} \right] \in \mathscr{S}$.
Axioms.
(1) $\mathord{\sim} \left[ \mathbf{A} \vee \mathbf{A} \right] \vee \mathbf{A}$
(2) $\mathord{\sim} \mathbf{A} \vee {}_\blacksquare \mathbf{B} \vee \mathbf{A}$
(3) $\mathord{\sim} \left[ \mathord{\sim} \mathbf{A} \vee \mathbf{B} \right] \vee {}_\blacksquare \mathord{\sim} \left[ \mathbf{C} \vee \mathbf{A} \right] \vee {}_\blacksquare \mathbf{B} \vee \mathbf{C}$

Defining $\supset$ as $\mathbf{A} \supset \mathbf{B}$ stands for $\mathord{\sim} \mathbf{A} \vee \mathbf{B}$, we can write these axioms as

(1) $\mathbf{A} \vee \mathbf{A} \supset \mathbf{A}$
(2) $\mathbf{A} \supset {}_\blacksquare \mathbf{B} \vee \mathbf{A}$
(3) $\mathbf{A} \supset \mathbf{B} \supset {}_\blacksquare \mathbf{C} \vee \mathbf{A} \supset {}_\blacksquare \mathbf{B} \vee \mathbf{C}$

$\mathscr{P}$ has one rule of inference:

Modus Ponens (MP). From $\mathbf{A}$ and $\mathord{\sim} \mathbf{A} \vee \mathbf{B}$ to infer $\mathbf{B}$.

More definitions needed to solve the exercise:

Def1. A proof of a wff $\mathbf{B}$ from the set $\mathscr{H}$ of hypotheses is a finite sequence $\mathbf{B}_1,\ldots,\mathbf{B}_m$ of wffs such that $\mathbf{B}_m$ is $\mathbf{B}$ and for each $j$ ($1 \leq j \leq m$) at least one of the following conditions is satisfied:
(1) $\mathbf{B}_j$ is an axiom.
(2) $\mathbf{B}_j$ is an member of $\mathscr{H}$.
(3) $\mathbf{B}_j$ is inferred by modus ponents from wffs $\mathbf{B}_i$ and $\mathbf{B}_k$, where $i < j$ and $k < j$.
Def2. A proof of a wff $\mathbf{B}$ is a proof of $\mathbf{B}$ from the emtpy set of hypotheses.
Def3. A theorem is a wff which has a proof.

 A: I'm sure that this sort of single axiom schema for propositional calculus was found by C. Meredith about 50 years ago. Google tells me that his original paper was  C. Meredith, Single axioms for the systems (C, N), (C, 0) and (A, N) of the two-valued propositional calculus, Journal of Computing Systems, p. 155-164, 1954. That paper will presumably give proofs that the axioms of some more familiar axiom systems can be derived from the single schema. 
However, this is a mere curiosity, and I've never seen any interest in this sort of brainteaser: what's the point? I'd just ignore this exercise in Andrews!
A: This sort of problem (not this problem though, at least not in the following link) appears on the metamath site. 
Ted Ulrich types this: "Can a fully-automated proof of the sufficiency of Meredith's 21-character single axiom, CCCCCpqCNrNsrtCCtpCsp [this isn't the same axiom as the original post, Meredith found a few single axioms which work for two-valued propositional logic] / ((((p⊃q)⊃(~r⊃~s))⊃r)⊃t)⊃((t⊃p)⊃(s⊃p)), for classical logic in C and N be found that equals (or shortens) Meredith's own derivation of Syl = CCpqCCqrCpr / ((p⊃q)⊃((q⊃r)⊃(p⊃r)), Scotus = CpCNpq / p⊃(~p⊃q), and Clavius = CCNppp / (~p⊃p)⊃p using just 41 condensed detachments?" 
Ted Ulrich continued " UPDATE: Larry Wos has (with OTTER) now discovered a proof using only 38 applications of condensed detachment. See Automated reasoning and the discovery of missing and elegant proofs, L. Wos and G. Peiper, Rinton, Paramus, 2003, sections 3.1 through 3.3."
There's plenty of other questions of this type that one can ask, since there exist several sets of axioms for classical propositional calculus.  Arthur Prior's textbook Formal Logic has three appendixes.  The first consists of postulate sets for logical calculi.  The second on methods of proof.  The preface to the second edition reads "There is also abundant material for exercises in simply verifying some of the relations asserted to hold between postulate-sets in this [the first] Appendix, using to this end, the techniques sketched in the one that follows it."
That these sorts of problems have gotten done have enabled us to know that there exist several different ways to approach propositional calculi axiomatically (even with only one axiom), even with axiom sets where every axiom is independent of every other axiom.
