It is not true.
Consider the lattices $\mathbf{M}_3,\mathbf{M}_4, \dots$ only with the language $\{\vee,\wedge\}$ instead of $\{\vee,\wedge,\neg\}$. First of all, one can show that $\mathbf{M}_n$ is simple for $n\geq 3$. Second of all, since the class of all lattices is a congruence distibutive variety, we can use Jonsson's lemma to say that the subdirectly irreducibles in $\mathsf{V}(\mathbf{M}_n)$ belong to $\mathsf{HS}(\mathbf{M}_n)$. Since the only sublattices of $\mathbf{M}_n$ are the lattices $\mathbf{M}_k$ for $k=0,1,2,\dots,n$, and each of those (except $\mathbf{M}_1$ and $\mathbf{M}_2$) are simple, we get that the subdirectly irreducibles in $\mathsf{V}(\mathbf{M}_n)$ are exactly $\mathbf{M}_0,\mathbf{M}_3,\dots,\mathbf{M}_n$.
So $\mathsf{V}(\mathbf{M}_m)$ is strictly contained in $\mathsf{V}(\mathbf{M}_n)$ whenever $3\leq m<n$. So, by Birkhoff's theorem, there must be some universally quantified equation $\forall v, \phi(v)=\chi(v)$ satisfied by $\mathbf{M}_m$ that is not satisfied by $\mathbf{M}_n$. So in $\mathbf{M}_n$ $\exists v,\phi(v)\neq\chi(v)$ (if $\phi(v)<\chi(v)$, then switch $\phi$ and $\chi$). Then $\phi\models_{\mathbf{M}_m}\chi$, but $\phi\not\models_{\mathbf{M}_n}\chi$. Since $\phi,\chi$ are formulas in $\{\vee,\wedge\}$, they are also formulas in $\{\vee,\wedge,\neg\}$.
As a specific example, $\mathbf{M}_3$ satisfies the equation
$
x_1\vee((x_2\vee(x_3\wedge x_4))\wedge(x_3\vee(x_1\wedge x_4)))\approx x_1\vee(((x_1\vee x_2)\vee(x_3\wedge x_4))\wedge(x_3\wedge(x_2\vee x_4)))
$
but $\mathbf{M}_4$ does not. Let
$\chi(x_1,x_2,x_3,x_4)=x_1\vee((x_2\vee(x_3\wedge x_4))\wedge(x_3\vee(x_1\wedge x_4)))$
and
$\phi(x_1,x_2,x_3,x_4)=x_1\vee(((x_1\vee x_2)\vee(x_3\wedge x_4))\wedge(x_3\wedge(x_2\vee x_4)))$
Now $\phi\models_{\mathbf{}_3}\chi$ since $\phi(v)$ always returns the same element as $\chi(v)$, but $\phi\not\models_{\mathbf{M}_4}\chi$ since $\chi(1,2,3,4)=1$ and $\phi(1,2,3,4)=\top$.
Best Answer
As $\neg \neg y \cong y$ for $y \in H$, it suffices to prove $\neg\neg(x \vee \neg x) \cong \top$. Now \[\neg(x \vee \neg x) \cong \neg x \land \neg \neg x \cong x\land \neg x \cong \bot\] (as the used de Morgan's law holds in Heyting algebras). And finally $\neg \bot \cong \top$.