Theorem 19.3t

Closed form of 19.3 and version of 19.9t with a universal quantifier. (Contributed by NM, 9-Nov-2020.) (Proof shortened by BJ, 9-Oct-2022.)

Conclusion
\( \vdash \Finv x \, \varphi \rightarrow (\forall x \, \varphi \leftrightarrow \varphi) \)
Proof
l0
sp
nf5r
impbid2 l0 _