  This paper studies a first-order expansion of a combination C+J of
intuitionistic and classical propositional logic, which was studied by
Humberstone (1979) and del Cerro and Herzig (1996), from a proof-theoretic
viewpoint. While C+J has both classical and intuitionistic implications, our
first-order expansion adds classical and intuitionistic universal quantifiers
and one existential quantifier to C+J. This paper provides a multi-succedent
sequent calculus G(FOC+J) for our combination of the first-order intuitionistic
and classical logic. Our sequent calculus G(FOC+J) restricts contexts of the
right rules for intuitionistic implication and intuitionistic universal
quantifier to particular forms of formulas. The cut-elimination theorem is
established to ensure the subformula property. As a corollary, G(FOC+J) is
conservative over both first-order intuitionistic and classical logic. Strong
completeness of G(FOC+J) is proved via a canonical model argument.
