Suppose that the axioms consist of the following three meaningful expressions, or correspond to the following three axioms if the formation rules get written differently:
Axiom Alternative Name
CxCyx C(x, C(y, x)) Recursive Letter Prefixing
CCxCyzCCxyCxz C(C(x, C(y, z)), C(C(x, y), C(x, z))) Conditional Distribution
CCNxNyCyx C(C(N(x), N(y)), C(y, x)) Transposed Negation Elimination
Suppose that the only rules of inference allow for consistent substitution for letters with meaningful expressions (substitution in a meaningful expression has to work out as uniform... if we substitute one letter with some meaningful expression in one spot in a meaningful expression, we have to substitute it with an equiform/"the same" meaningful expression in another spot), and detachment:
From $\vdash$C$\alpha$$\beta$ and $\vdash$$\alpha$ we may infer that $\vdash$$\beta$.
I will refer to CCxyCCNxyy or any correspondent meaningful expression as "Eliminated Excluded Middle" hereafter, since it can get obtained from the law of the excluded middle AxNx and CAxyCCxzCCyzz.
Eliminated Excluded Middle gets listed in A. N. Prior's appendix as an axiom in a system used by Hilbert in a 1922 text. Reading elsewhere suggests that the text is Hilbert and Ackermann's Grundzuge der theoretischen Logik (translated as "Principles of Mathematical Logic"). Mauro Allerganza used Eliminated Excluded Middle recently in an answer to another question. Eliminated Excluded Middle also got derived in Elliot Mendelson's Introduction to Mathematical Logic as the last part of Lemma 1.11 (g) on p. 38 and then used in the metalogical proof of the completeness theorem (did Kalmar also use Eliminated Excluded Middle?).
Can a proof of Eliminated Excluded Middle get proven from Recursive Letter Prefixing, Conditional Distribution, and Transposed Negation Elimination in less than or equal to 50 detachments?
Using an automated reasoning program it has suggested that it comes as possible to write a proof with 74 detachments, 73 detachments, 69 detachments, 113 detachments, 93 detachments, 75 detachments, 76 detachments, 124 detachments, 61 detachments, 60 detachments, 63 detachments, 68 detachments, 71 detachments, a distinct proof with 68 detachments, 72 detachments, a distinct proof with 61 detachments, a distinct proof with 74 detachments, 117 detachments, a distinct proof with 60 detachments, and to write a proof with 59 detachments of Eliminated Excluded Middle from the above 3 axioms.
Edit: The automated reasoning program has suggested some more proofs, including a proof with 58 detachments.
Edit 2: A 57 detachment proof also can get written.
At the end of this answer is a hyperresolution proof, used with permission, which Larry Wos obtained with the help of O.T.T.E.R.
Before that, though, I will display a proof of only 23 detachments with appropriate substitutions. This should not got interpreted as meaning that necessarily no shorter proof exists. The numerals in what follows only correspond to the proof below when a detachment gets made. There is no correspondence when a substitution gets made. Perhaps it is objectionable to do so during a course of a proof, but some different prefix notations will get used in the course of this demonstration. When in doubt as to how a notation works, we drop all parentheses and remove all spaces to see a form which fits with a definition suitable for the axioms.
Break...