Theorem
nfia1
Lemma 23 of [Monk2] p. 114. (Contributed by Mario Carneiro, 24-Sep-2016.)
Conclusion
\( \vdash \Finv x \, (\forall x \, \varphi \rightarrow \forall x \, \psi) \)
Proof
l0
nfa1
nfa1
nfim
l0
_
This is the content in the right pane.