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.