Theorem chvarvv

Implicit substitution of \( y' \) for \( x \) into a theorem. Version of chvarv with a disjoint variable condition, which does not require [ax-13]. (Contributed by NM, 20-Apr-1994.) (Revised by BJ, 31-May-2019.)

Hypotheses
chvarvv.1
\( \vdash x = y' \rightarrow (\varphi \leftrightarrow \psi) \)
chvarvv.2
\( \vdash \varphi \)
Conclusion
\( \vdash \psi \)
Proof
chvarvv.1
\( \vdash x = y' \rightarrow (\varphi \leftrightarrow \psi) \)
l1
spvv _
\( \vdash \forall x \, \varphi \rightarrow \psi \)
chvarvv.2
\( \vdash \varphi \)
mpg l1 _