Yes, but there is a broader class of formulas with the same property, which is the class that is usually considered. The class $\Sigma^0_1$ consists of formulas that use the same relations and operations in the question, any of the usual logical operations (including NOT and IMPLIES), and which can be put into the form
$$
(\exists x_1)\cdots(\exists x_n)\,\phi(x_1\ldots,x_n)
$$
where $\phi$ has no unbounded quantifiers ($\phi$ may have bounded universal quantifiers and may have bounded existential quantifiers).
Like the class of formulas in the question, these formulas can be proved by giving finitely many examples (values for $x_1,\ldots,x_n$) and then verifying that a formula with only bounded quantifiers is true, which can be done algorithmically.
The class $\Sigma^0_1$ is well known and significant in mathematical logic for several reasons:
A set of natural numbers is recursively enumerable if and only if it is definable by a $\Sigma^0_1$ formula. This relationship leads to applications of $\Sigma^0_1$ formulas in computability theory.
The proposition that a fixed effective formal theory is inconsistent can be written as a $\Sigma^0_1$ statement. This leads to applications of $\Sigma^0_1$ formulas in the proof theory of arithmetic, such as Gödel's incompleteness theorem.
A negation of a $\Sigma^0_1$ formula is called a $\Pi^0_1$ formula; $\Pi^0_1$ formulas can be disproved by giving finitely many examples and checking those examples. The classes $\Sigma^0_1$ and $\Pi^0_1$ sit close to the bottom of an infinite hierarchy of formulas known as the arithmetical hierarchy, and many properties of classes higher in the hierarchy follow from corresponding properties of the classes $\Sigma^0_1$ and $\Pi^0_1$.