Description: A 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). (Contributed by BJ, 4-Apr-2021)