Description: A weak variant of sbid2 not requiring ax-13 nor ax-10 . On top of Tarski's FOL, one implication requires only ax12v , and the other requires only sp . (Contributed by BJ, 25-May-2021)