 More astonishingly, Meredith (1951) showed that the whole of bivalent propositional calculus with quantifiers and variable functors can be deduced, using substitution, detachment and quantifier rules, from the single axiomatic formula