Axioms based on $\leftrightarrow, \lor, \bot$ for propositional intuitionistic logic? Propositional intuitionistic logic can be axiomatized based on $\;\to, \land, \lor, \bot\;$, with modus ponens
$$
\text{from }\; \phi \;\text{ and }\; \phi \to \psi \;\text{ infer }\; \psi
$$
as the only inference rule, and a list of axioms like
$$
\phi \to (\chi \to \phi )
$$
See the Wikipedia page on 'Intuitionistic logic' under 'Hilbert-style calculus' for a complete list of axioms.
Now that same page also claims that "{∨, ↔, ⊥} and {∨, ↔, ¬} are complete bases of intuitionistic connectives."  And what I am looking for is a list of inference rules and axioms to back up Wikipedia's claim.
Strictly speaking this is of course simple: one can take the $\;\to, \land, \lor, \bot\;$ axioms, and replace every $\;\phi \to \psi\;$ by $\;(\phi \lor \psi) \leftrightarrow \psi\;$, and every $\;\phi \land \psi\;$ by $\;(\phi \lor \psi) \leftrightarrow (\phi \leftrightarrow \psi)\;$.  But the result is not very elegant.
I've been puzzling a bit on constructing a nicer axiomatization, and I think it should at least have the inference rule
$$
\text{from }\; \phi \;\text{ and }\; \phi \leftrightarrow \psi \;\text{ infer }\; \psi
$$
and axioms like
$$
(\phi \leftrightarrow \psi) \;\leftrightarrow\; (\psi \leftrightarrow \phi)
\\
(\phi \leftrightarrow (\chi \leftrightarrow \psi)) \;\leftrightarrow\; ((\phi \leftrightarrow \chi) \leftrightarrow \psi)
$$
Therefore my question is: What is a complete and elegant axiomatization of propositional intuitionistic logic based on $\;\leftrightarrow, \lor, \bot\;$?
 A: How about a sequent calculus, with standard rules:
$$ \frac{\Gamma, P, P\vdash Q}{\Gamma, P\vdash Q}CL \qquad
\frac{}{\Gamma,P \vdash P}Ax  \qquad \frac{}{\Gamma, \bot \vdash P}{\bot}L $$
$$ \frac{\Gamma\vdash Q\quad \Gamma,P\vdash R}{\Gamma,P\leftrightarrow Q\vdash R}{\leftrightarrow}L_1
\quad \frac{\Gamma\vdash P\quad \Gamma,Q\vdash R}{\Gamma,P\leftrightarrow Q\vdash R}{\leftrightarrow}L_2
\quad \frac{\Gamma,P\vdash Q\quad \Gamma,Q\vdash P}{\Gamma\vdash P\leftrightarrow Q}{\leftrightarrow}R$$
$$ \frac{\Gamma,P\vdash R \quad \Gamma,Q\vdash R}{\Gamma,P\lor Q\vdash R}{\lor}L
\quad \frac{\Gamma\vdash P}{\Gamma\vdash P\lor Q}{\lor}R_1
\quad \frac{\Gamma\vdash Q}{\Gamma\vdash P\lor Q}{\lor}R_2 $$
This is complete for the $\{{\leftrightarrow},{\lor},\bot\}$ fragment because the full intuitionistic sequent calculus satisfies cut elimination.
To show that this fragment is complete in expressivity, express $P\to Q$ as $(P\lor Q)\leftrightarrow Q$ -- this equivalence is intuitionistically valid, and the usual left and right rules for $\to$ are easily built as combinations of the above rules.
Similarly, $\neg P$ is of course equivalent to $P\leftrightarrow \bot$.
For conjunction, contrary to speculation in comments, it turns out that $(P\lor Q)\leftrightarrow(P\leftrightarrow Q)$ is indeed intuitionistically equivalent to $P\land Q$. The difficult direction is to see that the usual ${\land}L$ rule is admissible, which can be done as follows in the above sequent calculus:
$$\begin{array}{rll}
0. & \Gamma,~ P,~ Q \vdash R & \text{premise of derived rule} \\
1. & P\vdash P\lor Q & \text{easy} \\
2. & P\leftrightarrow Q,~ P \vdash Q & \text{easy} \\
3. & (P\lor Q)\leftrightarrow(P\leftrightarrow Q),~ P \vdash Q & 1, 2, {\leftrightarrow}L_2 \\
4. & (P\lor Q)\leftrightarrow(P\leftrightarrow Q),~ Q \vdash P & \text{mutatis mutandis} \\
5. & (P\lor Q)\leftrightarrow(P\leftrightarrow Q) \vdash P\leftrightarrow Q & 3,4, {\leftrightarrow}R \\
6. & P\lor Q \vdash P\lor Q & \text{axiom} \\
7. & \Gamma,~ P\lor Q,~ P\leftrightarrow Q \vdash R & \text{easy consequence of }0 \\
8. & \Gamma,~ (P\lor Q)\leftrightarrow(P\leftrightarrow Q),~ P\lor Q \vdash R & 6,7, {\leftrightarrow}L_2 \\
9. & \Gamma,~ (P\lor Q)\leftrightarrow(P\leftrightarrow Q),~
     (P\lor Q)\leftrightarrow(P\leftrightarrow Q) \vdash R & 5,8, {\leftrightarrow}L_1 \\
10. & \Gamma,~ (P\lor Q)\leftrightarrow(P\leftrightarrow Q) \vdash R & 9, CL
\end{array}$$
(Proof found by exhaustive search!)

Or, for those that favor the Curry-Howard isomorphism for intuitionistic proofs, the idea in Haskell-like pseudosyntax for the ${\leftrightarrow}{\lor}{\bot}$ fragment is to replace
conj :: (P,Q)
let (x::P,y::Q) = conj
in  <..x..y..>

by
conj :: (Either P Q) <-> (P <-> Q)
let eq1 :: P <-> Q
    eq1 (x :: P) = let eq2 :: P <-> Q = conj (Left x) in eq2 x
    eq1 (y :: Q) = let eq2 :: P <-> Q = conj (Right y) in eq2 y
    disj :: Either P Q = conj eq1
in case disj of
     Left(x::P) -> let y::Q = eq1 x in <..x..y..>
     Right(y::Q) -> let x::P = eq1 y in <..x..y..>

where P <-> Q is supposed to behave like a function that can be applied to either P or Q and produces an output of the opposite type, and disjunction is represented by the standard Either type.
