Whenever I refer to an axiom set, unless stated otherwise, I presume the rule of detachemnt {|-Cab, |-a} -> b, where "a" and "b" constitute metavariables, and uniform substitution for variables.  The notation Da.b stands for a condensed detachment with "a" as the major premise and "b" as the minor premise.

Logical Formula of the Day: Cpp

Since this consists of a new thing I plan to do I guess I'll start small with one of the shortest tautologies in existence.  Cpp sometimes appears as an axiom in some propositional calculi.  For instance, A. N. Prior's formal logic lists {Cpp, CCCpqrCCrpCsCtp} as a basis for implicational propositional calculus.  It also appeared as an axiom in Peirce's axiom set for C-0 (0 meaning "falsum") classical logic {Cpp, CCpCqrCqCpr, CCpqCCqrCpr, C0p, CCCpqpp}.  In a natural deduction setting you can prove it as follows:

hypothesis 1 | p
Ci 1-1        2   Cpp

where "Ci" stands for conditional introduction.  For positive implicational propositional calculus with the axiom set {CpCqp, CCpCqrCCpqCpr} we can prove it in two condensed detachments.

axiom 1 CpCqp
axiom 2 CCpCqrCCpqCpr
D2.1   3 CCpqCpp
D3.1   4 Cpp

In classical logic with the basis {CCpqCCqrCCpr, CCNppp, CpCNpq} we can prove it in two steps also.

axiom 1 CCpqCCqrCpr
axiom 2 CCNppp
axiom 3 CpCNpq
D1.3   4 CCCNpqrCpr
D4.2   5 Cpp

Here's another proof from another axiom set:

axiom 1 CCCpqrCqr
axiom 2 CCCpqpp
D 1.2  3 Cpp

Actually, let's say we fix CCCpqrCqr as the first axiom 1.  Now replace the first p in CCCpqpp with CCpqp.  This yields CCCCCpqpqpp.  D1. CCCCCpqpqpp yields Cpp.  In any system sufficient for the conditional of classical logic, the variable "p" can get replaced by "CCpqp" since CCCpqpp is a theorem and CpCCpqp is also a theorem.  Consequently, we can iterate the process of replacing a "p" in any formula obtained in this way with CCCpqpp as the starting point and still obtain a theorem in classical logic, provided that we do NOT replace the last two "p's".  Each theorem obtained in this way serving as the minor premise along with CCCpqrCqr as the major premise will yield Cpp after a condensed detachment.

One can also prove it in Wajsberg-Lukasiewicz three-valued from the following basis as follows:

axiom 1 CpCqp
axiom 2 CCpqCCqrCpr
axiom 3 CCCpNppp
axiom 4 CCNpNqCqp
D2.1   5 CCCqprCpr
D5.3   6 Cpp

Or Lukasiewicz infinite valued-logic:

axiom     1 CpCqp
axiom     2 CCpqCCqrCpr
axiom     3 CCNpNqCqp
axiom     4 CCCpqqCCqpp
D2.1       5 CCCpqrCqr
D2.2       6 CCCCqrCprsCCpqs
D6.6       7 CCpCqrCCsqCpCsr
D5.4       8 CpCCpqq
C8.7       9 CCpCqrCqCpr
D9.1     10 CpCqq
D10.10 11 Cpp

Or from double suffixing CCpqCCqrCpr and the double negation laws CpNNp, CNNpp.

axiom   1 CCpqCCqrCpr
axiom   2 CpNNp
axiom   3 CNNpp
D1.2     4 CCNNpqCpq
D4.3     5 Cpp

Cpp as a major premise will only give you back the minor premise that you used when doing a condensed detachment.  On the other hand, Cpp as a minor premise has some interesting uses.  For instance D[CCpCqrCqCpr.Cpp] yields "modus ponens" CpCCpqq.  D[CCpCqrCCpqCpr.Cpp] yields CCCpqpCCpqq.  Perhaps more interestingly D[CCNpNqCCNpqq.Cpp] yields the law of Clavius CCNppp.  Additionally, if we consider D[CCpqCCqrCpr.a], and D[CCpqCCqrCpr.a] exists (which is equivalent to saying that "a" is a conditional), then D[D[CCpqCCqrCpr.a]].[Cpp] yields "a".