Theorem alrot4
Rotate four universal quantifiers twice. (Contributed by NM, 2-Feb-2005.)
(Proof shortened by Fan Zheng, 6-Jun-2016.)
Conclusion
\( \vdash \forall x \, \forall y \, \forall z \, \forall w \, \varphi \leftrightarrow \forall z \, \forall w \, \forall x \, \forall y \, \varphi \)
Proof
alrot3
l1
albii _
\( \vdash \forall x \, \forall y \, \forall z \, \forall w \, \varphi \leftrightarrow \forall x \, \forall z \, \forall w \, \forall y \, \varphi \)
alrot3
\( \vdash \forall x \, \forall z \, \forall w \, \forall y \, \varphi \leftrightarrow \forall z \, \forall w \, \forall x \, \forall y \, \varphi \)
bitri l1 _