Theorem chvar

Implicit substitution of \( y' \) for \( x \) into a theorem. Usage of this theorem is discouraged because it depends on [ax-13]. Use the weaker chvarfv if possible. (Contributed by Raph Levien, 9-Jul-2003.) (Revised by Mario Carneiro, 3-Oct-2016.) (New usage is discouraged.)

Hypotheses
chvar.1
\( \vdash \Finv x \, \psi \)
chvar.2
\( \vdash x = y' \rightarrow (\varphi \leftrightarrow \psi) \)
chvar.3
\( \vdash \varphi \)
Conclusion
\( \vdash \psi \)
Proof
l0
chvar.1
\( \vdash \Finv x \, \psi \)
chvar.2
biimpd _
\( \vdash x = y' \rightarrow \varphi \rightarrow \psi \)
l3
spim l0 _
\( \vdash \forall x \, \varphi \rightarrow \psi \)
chvar.3
\( \vdash \varphi \)
mpg l3 _