Theorem cbv3h

Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on [ax-13]. Use the weaker cbv3hv if possible. (Contributed by NM, 8-Jun-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 12-May-2018.) (New usage is discouraged.)

Hypotheses
cbv3h.1
\( \vdash \varphi \rightarrow \forall y \, \varphi \)
cbv3h.2
\( \vdash \psi \rightarrow \forall x \, \psi \)
cbv3h.3
\( \vdash x = y \rightarrow \varphi \rightarrow \psi \)
Conclusion
\( \vdash \forall x \, \varphi \rightarrow \forall y \, \psi \)
Proof
cbv3h.1
l1
nf5i _
cbv3h.2
l3
nf5i _
cbv3h.3
cbv3 l1 l3 _