Description: Proof of ax-8 from ax8v1 and ax8v2 , proving sufficiency of the
conjunction of the latter two weakened versions of ax8v , which is
itself a weakened version of ax-8 . (Contributed by BJ, 7-Dec-2020)(Proof shortened by Wolf Lammen, 11-Apr-2021)