 (2) A prenex formula \(A\) is derivable in the predicate calculus if and only if there is a disjunction \(\bigvee_j B_j\) of instances of the matrix of \(A\), such that \(\bigvee_j B_j\) is a quasi-tautology, and \(A\) is derivable from \(\bigvee_j B_j\) using the following rules: