Dijkstra and Scholten have proposed a formalization of
classical predicate logic on a novel deductive system as an
alternative to Hilbert's style of proof and Gentzen's
deductive systems. In this context we call it CED
(Calculus of Equational Deduction). This deductive
method promotes logical equivalence over implication and shows
that there are easy ways to prove predicate formulas without
the introduction of hypotheses or metamathematical tools such
as the deduction theorem. Moreover, syntactic considerations
(in Dijkstra's words, "letting the symbols do the work") have
led to the "calculational style," an impressive array of
techniques for elegant proof constructions. In this paper, we
formalize intuitionistic predicate logic according to
CED with similar success. In this system
(I-CED), we prove Leibniz's principle for
intuitionistic logic and also prove that any (intuitionistic)
valid formula of predicate logic can be proved in
I-CED.