Define a propositional form as follows:

1) Lower case letters, along with lower case letters subscripted with numbers a₁, b₂, c₁₃ are propositional forms.

2) If x and y are both propositional forms, then Cxy is a propositional form.

Let Cab denote the material conditional with 'a' and 'b' taking truth values in {T, F}. Let "C₁ ...C_n" denote a concatenation of n conditionals, and "a₁...a_(n+1)" a concatenation of (n+1) logical variables. E. G. C₁...C₃a₁...a₄ denotes CCCa₁a₂a₃a₄. Let a/b denote a substitution of variable "a" with "b", let a/Cab denote that we substitute variable "a" with Cab.

Axiom 1: CCpqCCqrCpr

Axiom 2: CqCpq

Theorem 1: CCCpqC₁...C_(10^100)a₁...a_((10^100)+1)CqC₁...C_(10^100)a₁...a_((10^100)+1)

Demonstration:

1 CCqCpqCCCpqC₁...C_(10^100)a₁...a_((10^100)+1)CqC₁...C_(10^100)
a₁...a_((10^100)+1) Axiom 1, p/q, q/Cpq, r/C₁...C_(10^100)a₁...a_((10^100)+1)

2 CCCpqC₁...C_(10^100)a₁...a_((10^100)+1)CqC₁...C_(10^100)a₁...a_((10^100)+1) Axiom 2, 1 detachment.