Theorem stdpc5v

Version of stdpc5 with a disjoint variable condition, requiring fewer axioms. (Contributed by BJ, 7-Mar-2020.) Revised to shorten 19.21v. (Revised by Wolf Lammen, 12-Jul-2020.)

Conclusion
\( \vdash \forall x \, (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \forall x \, \psi \)
Proof
l0
ax-5
\( \vdash \varphi \rightarrow \forall x \, \varphi \)
alim
\( \vdash \forall x \, (\varphi \rightarrow \psi) \rightarrow \forall x \, \varphi \rightarrow \forall x \, \psi \)
syl5 l0 _