Description: Another single axiom for minimal implicational calculus, due to Meredith.
Other single axioms of the same length are known, but it is thought to be
the minimal length. Among single axioms of this length, it is the one
with simplest antecedents (i.e., in the corresponding ordering of binary
trees which first compares left subtrees, it is the first one). Known as
"HI-2" on Dolph Edward "Ted" Ulrich's web page. In the next 4 lemmas and
5 theorems, ax-1 and ax-2 are derived from this other single axiom in
20 detachments (instances of ax-mp ) in total. Polish prefix notation:
CpCCqrCCCsqCrtCqt ; or CtCCpqCCCspCqrCpr in Carew Arthur Meredith and
Arthur Norman Prior,Notes on the axiomatics of the propositional
calculus, Notre Dame Journal of Formal Logic, volume IV, number 3, July
1963, pages 171--187, on page 180. (Contributed by BJ, 4-Apr-2021)(Revised by ADH, 10-Nov-2023)