Formula of the Day: EEEpqrEpEqr

EEEpqrEpEqr comes as a way of saying that logical equivalence associates.  Along with EEpqEqp can serve as one of the axioms of the equivalential calculus.  Equivalential calculus allows us to deduce all tautologies which only have equivalence symbols and variables in them.  The rule of inference for equivalential calculus comes as a modified form of detachment "from Eab, as well as "a", we may infer b" where "a" and "b" consist of meta-variables.  Or more compactly

{Eab, a} -> b

We can condensed such an E-detachment along with uniform substitution just like we can condense C-detachment with uniform substitution.  Taking EEEpqrEpEqr as an axiom, we can develop the system {EEEpqrEpEqr} as follows:

axiom 1 EEEpqrEpEqr
D1.1   2 EEpqErEpEqr
D1.2   3 EpEqErEpEqr
D2.1   4 EsEEEpqrEEpEqrs
D1.3   5 EpEqErEsEEpqErs
D1.4   6 EpEqEEErstEErEstEpq
D2.2   7 EpEEqrEEsEqErsp
D2.3   8 EsEpEEqErEpEqrs

The system with a single axiom which corresponds to each of these theorems has no last theorem under condensed detachment (unlike {Cpp} which has Cpp as its only theorem under condensed detachment).  For {EEpqErEpEqr} each theorem will have some form Eab, which implies that there exists a substitution which enables a detachment from the antecedent of Epq of EEpqErEpEqr with EEpqErEpEqr as the major premise, and any theorem of the system {EEpqErEpEqr}.  For the systems corresponding to theorems 3 through 8, each axiom serving as the major premise and any theorem serving as the minor premise enables a condensed detachment.  Does *every* theorem EEEpqrEpEqr correspond to a system with a sole axiom which has no last theorem under condensed detachment?

EEEpqrEpEqr seems to come as a theorem that requires a fair amount of work to prove in the natural deduction systems I've encountered and in non-equivalential systems of logic which use definitions to get equivalences into the system.