Theorem cbvalivw

Change bound variable. Uses only Tarski's FOL axiom schemes. Part of Lemma 7 of [KalishMontague] p. 86. (Contributed by NM, 9-Apr-2017.)

Hypothesis
cbvalivw.1
\( \vdash x = y \rightarrow \varphi \rightarrow \psi \)
Conclusion
\( \vdash \forall x \, \varphi \rightarrow \forall y \, \psi \)
Proof
cbvalivw.1
\( \vdash x = y \rightarrow \varphi \rightarrow \psi \)
spimvw _
alrimiv _