Theorem con4

Alias for [ax-3] to be used instead of it for labeling consistency. Its associated inference is con4i and its associated deduction is con4d. (Contributed by BJ, 24-Dec-2020.)

Conclusion
\( \vdash (\neg \varphi \rightarrow \neg \psi) \rightarrow \psi \rightarrow \varphi \)
Proof
ax-3