Description: Show that the original axiom ax-c7 can be derived from ax-10 ( hbn1 ) , sp and propositional calculus. See ax10fromc7 for the
rederivation of ax-10 from ax-c7 .

Normally, axc7 should be used rather than ax-c7 , except by theorems
specifically studying the latter's properties. (Contributed by NM, 21-May-2008)