Theorem ax5d

Version of [ax-5] with antecedent. Useful in proofs of deduction versions of bound-variable hypothesis builders. (Contributed by NM, 1-Mar-2013.)

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