Description: Formula-building lemma for use with the Distinctor Reduction Theorem.
Part of Theorem 9.4 of Megill p. 448 (p. 16 of preprint). Usage of
this theorem is discouraged because it depends on ax-13 . Usage of
exbidv is preferred, which requires fewer axioms. (Contributed by NM, 27-Feb-2005)(New usage is discouraged.)