Here's my thirteen-step derivation of CCCpqCCrpCrqCss /  {(p→q)→[(r→p)→(r→q)]}→(s→s) from the axioms B, C, and I*: 1. CCpqCCrpCrq                   B       (p→q)→[(r→p)→(r→q)]                 2. CCpCqrCqCpr                   C       [p→(q→r)]→[q→(p→r)]                    3. CCppCqq                             I*     (p→p)→(q→q) D1.1     =   4. CCpCqrCpCCsqCsr                    [p→(q→r)]→{p→[(s→q)→(s→r)]} D1.2     =   5. CCpCqCrsCpCrCqs                   {p→[q→(r→s)]}→{p→[r→(q→s)]} D2.1     =   6. CCpqCCqrCpr                             (p→q)→[(q→r)→(p→r)] D1.3     =   7. CCpCqqCpCrr                              [p→(q→q)]→[p→(r→r)] D5.5     =   8. CCpCqCrsCrCpCqs                   {p→[q→(r→s)]}→{r→[p→(q→s)]} D5.4     =   9. CCpCqrCCsqCpCsr                    [p→(q→r)]→{(s→q)→[p→(s→r)]} D5.7     = 10. CCpCqqCrCpr                              [p→(q→q)]→[r→(p→r)] D1.7      = 11. CCpCqCrrCpCqCss                    {p→[q→(r→r)]}→{p→[q→(s→s)]} D6.8        =  12. CCCpCqCrstCCqCrCpst                     [{p→[q→(r→s)]}→t]→[{q→[r→(p→s)]}→t] D9.9     = 13. CCpCqrCCsCrtCpCsCqt           [p→(q→r)]→[[s→(r→t)]→{p→[s→(q→t)]}] D12.10 = 14. CCCpqCpCrqCsCrs                   {(p→q)→[p→(r→q)]}→[s→(r→s)] D11.13 = 15. CCCpCqrCqsCCpCsrCtt           {[p→(q→r)]→(q→s)}→{[p→(s→r)]→(t→t)} D15.14 = 16. CCCpqCCrpCrqCss              {(p→q)→[(r→p)→(r→q)]}→(s→s) © Dolph Ulrich, 2007