Theorem
sylgt
Closed form of
sylg
. (Contributed by BJ, 2-May-2019.)
Conclusion
\( \vdash \forall x \, (\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \forall x \, \psi) \rightarrow \varphi \rightarrow \forall x \, \chi \)
Proof
alim
imim2d
_
This is the content in the right pane.