Theorem axc4i

Inference version of axc4. (Contributed by NM, 3-Jan-1993.)

Hypothesis
axc4i.1
\( \vdash \forall x \, \varphi \rightarrow \psi \)
Conclusion
\( \vdash \forall x \, \varphi \rightarrow \forall x \, \psi \)
Proof
l0
nfa1
axc4i.1
alrimi l0 _