Theorem bj-cbvalimdv

Description: A lemma for alpha-renaming of variables bound by a universal quantifier. (Contributed by BJ, 4-Apr-2026) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	bj-cbvalimdv.nf0	$$⊢\phi \to \forall x\phi$$
	bj-cbvalimdv.nf1	$$⊢\phi \to \forall y\phi$$
	bj-cbvalimdv.nfth	$$⊢\phi \to \left(\exists x\theta \to \theta \right)$$
	bj-cbvalimdv.denote	$$⊢\phi \to \forall y\exists x\psi$$
	bj-cbvalimdv.maj	$$⊢\left(\phi \wedge \psi \right)\to \left(\chi \to \theta \right)$$
Assertion	bj-cbvalimdv	$$⊢\phi \to \left(\forall x\chi \to \forall y\theta \right)$$

Proof

Step	Hyp	Ref	Expression
1		bj-cbvalimdv.nf0	$$⊢\phi \to \forall x\phi$$
2		bj-cbvalimdv.nf1	$$⊢\phi \to \forall y\phi$$
3		bj-cbvalimdv.nfth	$$⊢\phi \to \left(\exists x\theta \to \theta \right)$$
4		bj-cbvalimdv.denote	$$⊢\phi \to \forall y\exists x\psi$$
5		bj-cbvalimdv.maj	$$⊢\left(\phi \wedge \psi \right)\to \left(\chi \to \theta \right)$$
6		ax5d	$$⊢\phi \to \left(\forall x\chi \to \forall y\forall x\chi \right)$$
7	1 2 6 3 4 5	bj-cbvalimdlem	$$⊢\phi \to \left(\forall x\chi \to \forall y\theta \right)$$