Prove double negation introduction WITHOUT elimination, in a propositional logic axiom system.

Question

I'm looking for a proof in classical propositional logic of "double negation introduction" (Q⊢¬¬Q) without using double negation elimination (¬¬Q⊢Q).

I'm using the Hilbert system with the following axioms:

1. X→(Y→X)

2. (X→(Y→Z))→((X→Y)→(X→Z))

3. (¬Y→¬X)→(X→Y)

Use uniform substitution and Modes Ponens as rule of inference. Deduction Theorem also allowed.

Prove (Q⊢¬¬Q) without assuming (¬¬Q⊢Q). Thanks!

Remark: I know that this is possible, by the fact that only (Q⊢¬¬Q) is valid in intuitionistic logic; (¬¬Q⊢Q) is not. Therefore one should be able to derive (Q⊢¬¬Q) without using (¬¬Q⊢Q) since the former, and not the latter, holds in weaker systems than classical logic. However, all the proofs I've seen so far use (¬¬Q⊢Q).