Theorem alrot3
Theorem *11.21 in [WhiteheadRussell] p. 160. (Contributed by Andrew
Salmon, 24-May-2011.)
Conclusion
\( \vdash \forall x \, \forall y \, \forall z \, \varphi \leftrightarrow \forall y \, \forall z \, \forall x \, \varphi \)
Proof
l0
alcom
\( \vdash \forall x \, \forall y \, \forall z \, \varphi \leftrightarrow \forall y \, \forall x \, \forall z \, \varphi \)
alcom
albii _
\( \vdash \forall y \, \forall x \, \forall z \, \varphi \leftrightarrow \forall y \, \forall z \, \forall x \, \varphi \)
bitri l0 _