Theorem alim

Restatement of Axiom [ax-4], for labeling consistency. It should be the only theorem using [ax-4]. (Contributed by NM, 10-Jan-1993.)

Conclusion

\( \vdash \forall x \, (\varphi \rightarrow \psi) \rightarrow \forall x \, \varphi \rightarrow \forall x \, \psi \)

Proof

ax-4