Use of quantifier movement in mathematical proofs

Question

Are there any mathematical theorems that make use of the following quantifier movement laws in their proofs? $$\big((\forall x)(\varphi(x) \rightarrow \psi ) \big) \iff \big(\exists x\varphi(x) \rightarrow \psi \big) $$ $$\big((\exists x)(\varphi(x) \rightarrow \psi ) \big) \iff \big(\forall x\varphi(x) \rightarrow \psi \big) $$ I have never encountered them in any proof uptil now (or maybe I did but I was not made aware of it) even though the laws seem to be very powerful.

Answer 1

In "natural-language" proofs I've not seen either of these arise. This is because the left hand sides of each equivalence are rather unnatural statements which lean rather heavily on the less intuitive nature of material implication (a la the drinker paradox).

Of course that says nothing about their appearance in formal proofs, where I do suspect that such quantifier juggling occurs from time to time. I don't have an example off the top of my head, though; while I know a fair bit about the general theory of formal proofs, I know rather little about specific examples and techniques, so I don't have a meaningful body of cases to draw on.

But since we tend (reasonably, in my opinion) to focus more on "informal-but-rigorous" proofs, I'd say the answer to your question is no (although that's inherently hard to demonstrate convincingly), for the stronger reason that the left hand sides aren't even going to crop up at all in a well-written natural-language argument.

---

Of course this is excluding theorems about logical forms themselves - e.g. those very equivalences. I consider such examples trivial as far as this question goes (although not trivial in a broad sense).