Are there more identities of this sort (http://en.wikipedia.org/wiki/First-order_logic#Provable_identities) that are interesting/non-trivial? It seems that most further work in first-order logic is metalogical, but I wonder how much more there is to understand in the logic. Interesting boolean identities would also satisfy this question.
Of course there are.
Basically, they are inter-derivable form the corresponding ones with $\land$ and $\lor$.
Are them interesting ?
In the foolowing book : George Tourlakis, Mathematical Logic (2008), the mathematical logic is treated as an equational calculus, i.e. with $\leftrightarrow$ (or $\equiv$) as "basic" connective.
There you can find a huge amount of "identities" with their proof.