Theorem chvarv

Implicit substitution of \( y' \) for \( x \) into a theorem. Usage of this theorem is discouraged because it depends on [ax-13]. Use the weaker chvarvv if possible. (Contributed by NM, 20-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Apr-2018.) (New usage is discouraged.)

Hypotheses
chvarv.1
\( \vdash x = y' \rightarrow (\varphi \leftrightarrow \psi) \)
chvarv.2
\( \vdash \varphi \)
Conclusion
\( \vdash \psi \)
Proof
l0
nfv
\( \vdash \Finv x \, \psi \)
l1
chvarv.1
\( \vdash x = y' \rightarrow (\varphi \leftrightarrow \psi) \)
chvarv.2
\( \vdash \varphi \)
chvar l0 l1 _