Theorem cbv3

Rule used to change bound variables, using implicit substitution, that does not use [ax-c9]. Usage of this theorem is discouraged because it depends on [ax-13]. Use the weaker cbv3v if possible. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 12-May-2018.) (New usage is discouraged.)

Hypotheses
cbv3.1
\( \vdash \Finv y \, \varphi \)
cbv3.2
\( \vdash \Finv x \, \psi \)
cbv3.3
\( \vdash x = y \rightarrow \varphi \rightarrow \psi \)
Conclusion
\( \vdash \forall x \, \varphi \rightarrow \forall y \, \psi \)
Proof
cbv3.1
nf5ri _
l2
hbal _
l3
cbv3.2
\( \vdash \Finv x \, \psi \)
cbv3.3
\( \vdash x = y \rightarrow \varphi \rightarrow \psi \)
spim l3 _
alrimih l2 _