Description: Proof of a single axiom that can replace ax-c5 , ax-c7 , and ax-11 in a subsystem that includes these axioms plus ax-c4 and ax-gen (and
propositional calculus). See axc5c711toc5 , axc5c711toc7 , and
axc5c711to11 for the rederivation of those axioms. This theorem extends
the idea in Scott Fenton's axc5c7 . (Contributed by NM, 18-Nov-2006)(Proof modification is discouraged.)(New usage is discouraged.)