Description: Version of cbv3h with two disjoint variable conditions, which does not require ax-11 nor ax-13 . (Contributed by BJ, 24-Jun-2019) (Proof modification is discouraged.)