Theorem cbv1h
Rule used to change bound variables, using implicit substitution. Usage
of this theorem is discouraged because it depends on [ax-13].
(Contributed by NM, 11-May-1993.) (Proof shortened by Wolf Lammen,
13-May-2018.) (New usage is discouraged.)
Hypotheses
cbv1h.1
\( \vdash \varphi \rightarrow \psi \rightarrow \forall y \, \psi \)
cbv1h.2
\( \vdash \varphi \rightarrow \chi \rightarrow \forall x \, \chi \)
cbv1h.3
\( \vdash \varphi \rightarrow x = y \rightarrow \psi \rightarrow \chi \)
Conclusion
\( \vdash \forall x \, \forall y \, \varphi \rightarrow \forall x \, \psi \rightarrow \forall y \, \chi \)
Proof
l0
nfa1
l1
nfa2
l2
2sp
\( \vdash \forall x \, \forall y \, \varphi \rightarrow \varphi \)
cbv1h.1
\( \vdash \varphi \rightarrow \psi \rightarrow \forall y \, \psi \)
syl l2 _
l5
nf5d l1 _
cbv1h.2
\( \vdash \varphi \rightarrow \chi \rightarrow \forall x \, \chi \)
syl l2 _
l8
nf5d l0 _
cbv1h.3
\( \vdash \varphi \rightarrow x = y \rightarrow \psi \rightarrow \chi \)
syl l2 _
cbv1 l0 l1 l5 l8 _