Over the years, proof systems for propositional satisfiability (SAT)have been extensively studied. Recently, proof systems forquantified Boolean formulas (QBFs) have also been gaining attention.Q-resolution is a calculus enabling producing proofs fromDPLL-based QBF solvers. While DPLL has become a dominating techniquefor SAT, QBF has been tackled by other complementary and competitiveapproaches. One of these approaches is based on expanding variablesuntil the formula contains only one type of quantifier; upon which aSAT solver is invoked. This approach motivates the theoreticalanalysis carried out in this paper. We focus on a two phase proof system,which expands the formula in the first phase and applies propositionalresolution in the second. Fragments of this proof system are defined andcompared to Q-resolution.