On axiom systems of propositional calculi, IV
Kiyoshi Iséki · Proceedings of the Japan Academy Series A Mathematical Sciences · 1965
1 CpCqp, 2 CCpCqrCCpqCpr, 3 CCNpNqCCNpqp.E. Mendelson 5 proved some tautologies by using the rules of inference and a metatheorem known as Herbrand deduction theorem: If / is a set of theses and p, q are theses and F, p-q, then