Theorem bj-cbvalim

Description: A lemma used to prove bj-cbval in a weak axiomatization. (Contributed by BJ, 12-Mar-2023) (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-cbvalim	$$⊢\forall y\exists x\chi \to \left(\forall y\forall x\left(\chi \to \left(\phi \to \psi \right)\right)\to \left(\forall x\phi \to \forall y\psi \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		ax5e	$$⊢\exists x\psi \to \psi$$
2	1	ax-gen	$$⊢\forall y\left(\exists x\psi \to \psi \right)$$
3		ax-5	$$⊢\forall x\phi \to \forall y\forall x\phi$$
4		bj-cbvalimt	$$⊢\forall y\exists x\chi \to \left(\forall y\forall x\left(\chi \to \left(\phi \to \psi \right)\right)\to \left(\left(\forall x\phi \to \forall y\forall x\phi \right)\to \left(\forall y\left(\exists x\psi \to \psi \right)\to \left(\forall x\phi \to \forall y\psi \right)\right)\right)\right)$$
5	4	com3l	$$⊢\forall y\forall x\left(\chi \to \left(\phi \to \psi \right)\right)\to \left(\left(\forall x\phi \to \forall y\forall x\phi \right)\to \left(\forall y\exists x\chi \to \left(\forall y\left(\exists x\psi \to \psi \right)\to \left(\forall x\phi \to \forall y\psi \right)\right)\right)\right)$$
6	5	com14	$$⊢\forall y\left(\exists x\psi \to \psi \right)\to \left(\left(\forall x\phi \to \forall y\forall x\phi \right)\to \left(\forall y\exists x\chi \to \left(\forall y\forall x\left(\chi \to \left(\phi \to \psi \right)\right)\to \left(\forall x\phi \to \forall y\psi \right)\right)\right)\right)$$
7	2 3 6	mp2	$$⊢\forall y\exists x\chi \to \left(\forall y\forall x\left(\chi \to \left(\phi \to \psi \right)\right)\to \left(\forall x\phi \to \forall y\psi \right)\right)$$