Theorem cbval

Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on [ax-13]. Check out cbvalw, cbvalvw, cbvalv1 for versions requiring fewer axioms. (Contributed by NM, 13-May-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) (New usage is discouraged.)

Hypotheses
cbval.1
\( \vdash \Finv y \, \varphi \)
cbval.2
\( \vdash \Finv x \, \psi \)
cbval.3
\( \vdash x = y \rightarrow (\varphi \leftrightarrow \psi) \)
Conclusion
\( \vdash \forall x \, \varphi \leftrightarrow \forall y \, \psi \)
Proof
l0
cbval.1
l1
cbval.2
cbval.3
biimpd _
l4
cbv3 l0 l1 _
l5
cbval.2
l6
cbval.1
cbval.3
biimprd _
equcoms _
cbv3 l5 l6 _
impbii l4 _