# Metamath Proof Explorer

## Theorem cbvaliw

Description: Change bound variable. Uses only Tarski's FOL axiom schemes. Part of Lemma 7 of KalishMontague p. 86. (Contributed by NM, 19-Apr-2017)

Ref Expression
Hypotheses cbvaliw.1 ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }$
cbvaliw.2 ${⊢}¬{\psi }\to \forall {x}\phantom{\rule{.4em}{0ex}}¬{\psi }$
cbvaliw.3 ${⊢}{x}={y}\to \left({\phi }\to {\psi }\right)$
Assertion cbvaliw ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {y}\phantom{\rule{.4em}{0ex}}{\psi }$

### Proof

Step Hyp Ref Expression
1 cbvaliw.1 ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }$
2 cbvaliw.2 ${⊢}¬{\psi }\to \forall {x}\phantom{\rule{.4em}{0ex}}¬{\psi }$
3 cbvaliw.3 ${⊢}{x}={y}\to \left({\phi }\to {\psi }\right)$
4 2 3 spimw ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\to {\psi }$
5 1 4 alrimih ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {y}\phantom{\rule{.4em}{0ex}}{\psi }$