Theorem cbv3v2

Version of cbv3 with two disjoint variable conditions, which does not require [ax-11] nor [ax-13]. (Contributed by BJ, 24-Jun-2019.) (Proof shortened by Wolf Lammen, 30-Aug-2021.)

Hypotheses
cbv3v2.nf
\( \vdash \Finv x \, \psi \)
cbv3v2.1
\( \vdash x = y \rightarrow \varphi \rightarrow \psi \)
Conclusion
\( \vdash \forall x \, \varphi \rightarrow \forall y \, \psi \)
Proof
l0
cbv3v2.nf
\( \vdash \Finv x \, \psi \)
cbv3v2.1
\( \vdash x = y \rightarrow \varphi \rightarrow \psi \)
spimfv l0 _
alrimiv _