Theorem bj-sylggt

Description: Stronger form of sylgt , closer to ax-2 . (Contributed by BJ, 30-Jul-2025)

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

Proof

Step	Hyp	Ref	Expression
1		alim	$$⊢\forall x\left(\psi \to \chi \right)\to \left(\forall x\psi \to \forall x\chi \right)$$
2	1	imim3i	$$⊢\left(\phi \to \forall x\left(\psi \to \chi \right)\right)\to \left(\left(\phi \to \forall x\psi \right)\to \left(\phi \to \forall x\chi \right)\right)$$