Theorem nfa2

Lemma 24 of [Monk2] p. 114. (Contributed by Mario Carneiro, 24-Sep-2016.) Remove dependency on [ax-12]. (Revised by Wolf Lammen, 18-Oct-2021.)

Conclusion
\( \vdash \Finv x \, \forall y \, \forall x \, \varphi \)
Proof
l0
alcom
\( \vdash \forall y \, \forall x \, \varphi \leftrightarrow \forall x \, \forall y \, \varphi \)
nfa1
\( \vdash \Finv x \, \forall x \, \forall y \, \varphi \)
nfxfr l0 _