Theorem pm11.53

Theorem *11.53 in [WhiteheadRussell] p. 164. See pm11.53v for a version requiring fewer axioms. (Contributed by Andrew Salmon, 24-May-2011.)

Conclusion
\( \vdash \forall x \, \forall y \, (\varphi \rightarrow \psi) \leftrightarrow \exists x \, \varphi \rightarrow \forall y \, \psi \)
Proof
19.21v
l1
albii _
\( \vdash \forall x \, \forall y \, (\varphi \rightarrow \psi) \leftrightarrow \forall x \, (\varphi \rightarrow \forall y \, \psi) \)
nfv
nfal _
19.23 _
\( \vdash \forall x \, (\varphi \rightarrow \forall y \, \psi) \leftrightarrow \exists x \, \varphi \rightarrow \forall y \, \psi \)
bitri l1 _