Theorem cbv3hv

Rule used to change bound variables, using implicit substitution. Version of cbv3h with a disjoint variable condition on x , y, which does not require [ax-13]. Was used in a proof of axc11n (but of independent interest). (Contributed by NM, 25-Jul-2015.) (Proof shortened by Wolf Lammen, 29-Nov-2020.) (Proof shortened by BJ, 30-Nov-2020.)

Hypotheses
cbv3hv.nf1
\( \vdash \varphi \rightarrow \forall y \, \varphi \)
cbv3hv.nf2
\( \vdash \psi \rightarrow \forall x \, \psi \)
cbv3hv.1
\( \vdash x = y \rightarrow \varphi \rightarrow \psi \)
Conclusion
\( \vdash \forall x \, \varphi \rightarrow \forall y \, \psi \)
Proof
cbv3hv.nf1
l1
nf5i _
cbv3hv.nf2
l3
nf5i _
cbv3hv.1
cbv3v l1 l3 _