I am too removed from the subject these days, so my answer might be not very insightful (but I hope experts will help here). If you are willing to admit quantifiers (which appear in some proof systems), you may end up with an equivalential calculus resembling Le'sniewski's protothetics (you might want to check his mereology and ontology as well, as you are interested in equality of terms whose "constructors" coincide). Quoting from the Stanford Encyclopedia of Philosophy, http://plato.stanford.edu/entries/lesniewski/
``Le'sniewski's preference for an axiom system, based in part on the success of Ontology, and also on considerations about the nature of definition, was to base a logical system on the single connective of material equivalence, together with the universal quantifier. He was held up for some time in doing this for Protothetic by his inability to see how to eliminate the connective of conjunction in terms of equivalence. Given quantification and equivalence, negation is easy to define, in a way Russell once suggested to Frege:
$\rm{Def. }\ \sim$ : $\forall p\ulcorner \sim p \leftrightarrow (p \leftrightarrow \forall r \ulcorner r\urcorner)\urcorner$
The solution was found for Le'sniewski by his 21-year-old doctoral student Alfred Teitelbaum, later renowned under his adopted name as Alfred Tarski. It consisted in quantifying not just sentences but sentential functions or connectives:
$\rm{Def.}\ \wedge: \forall pq\ulcorner p \wedge q \leftrightarrow \forall f\ulcorner p \leftrightarrow (f(p) \leftrightarrow f(q))\urcorner \urcorner$
in this case, quantifying one-place connectives. Assuming there are just four of these connectives, assertion, negation, Verum (tautology) and Falsum (contradiction), it is straightforward to show that the right-hand side is equivalent to the conjunction of p and q. Tarski's doctoral dissertation centres around this result.
As to axiomatization, Le'sniewski knew that the pure theory of equivalence could be based on two axioms stating skew-transitivity and associativity:
$P1 \quad ((p \leftrightarrow r)\leftrightarrow (q \leftrightarrow p)) \leftrightarrow (r \leftrightarrow q)$
$P2 \quad (p \leftrightarrow (q\leftrightarrow r)) \leftrightarrow ((p \leftrightarrow q) \leftrightarrow↔ r)$.
Pure equivalential calculus has the quaint property, shown by Le'sniewski, that a formula is a theorem if and only if every propositional variable in it occurs an even number of times."
I make this CW, first because I am not an expert; second, because it seems I could use some help on TeX, which is acting up...