We establish a framework to integrate propositional logic with
first-order logic. This is done in such a way that it optionally
appears either as first-order logic over a Boolean algebra or as
propositional logic including Boolean quantification. We describe and
prove complexity bounds for extended quantifier elimination by virtual
substitution for our theory. This extended quantifier elimination is,
besides many other mathematical algorithms and utilities, implemented
in a new context \textsc{ibalp} of the \textsc{reduce} package
\textsc{redlog}. We demonstrate the capabilities of this new context
by means of numerous application and benchmark examples including
\textsc{qsat} problems.