Theorem bj-exalim

Description: Distribute quantifiers over a nested implication.

This and the following theorems are the general instances of already proved theorems. They could be moved to the main part, before ax-5 . I propose to move to the main part: bj-exalim , bj-exalimi , bj-exalims , bj-exalimsi , bj-ax12i , bj-ax12wlem , bj-ax12w , and remove equs3OLD . A new label is needed for bj-ax12i and label suggestions are welcome for the others. I also propose to change -. A. x -. to E. x in speimfw and spimfw (other spim* theorems use E. x and very few theorems in set.mm use -. A. x -. ). (Contributed by BJ, 8-Nov-2021)

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

Proof

Step	Hyp	Ref	Expression
1		pm2.04	$$⊢\left(\phi \to \left(\psi \to \chi \right)\right)\to \left(\psi \to \left(\phi \to \chi \right)\right)$$
2	1	alimi	$$⊢\forall x\left(\phi \to \left(\psi \to \chi \right)\right)\to \forall x\left(\psi \to \left(\phi \to \chi \right)\right)$$
3		bj-alexim	$$⊢\forall x\left(\psi \to \left(\phi \to \chi \right)\right)\to \left(\forall x\psi \to \left(\exists x\phi \to \exists x\chi \right)\right)$$
4		pm2.04	$$⊢\left(\forall x\psi \to \left(\exists x\phi \to \exists x\chi \right)\right)\to \left(\exists x\phi \to \left(\forall x\psi \to \exists x\chi \right)\right)$$
5	2 3 4	3syl	$$⊢\forall x\left(\phi \to \left(\psi \to \chi \right)\right)\to \left(\exists x\phi \to \left(\forall x\psi \to \exists x\chi \right)\right)$$