Theorem ralimralim

Description: Introducing any antecedent in a restricted universal quantification. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Assertion	ralimralim	$$⊢\forall x\in A\phi \to \forall x\in A\left(\psi \to \phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		nfra1	$$⊢Ⅎx\forall x\in A\phi$$
2		rspa	$$⊢\left(\forall x\in A\phi \wedge x\in A\right)\to \phi$$
3		ax-1	$$⊢\phi \to \left(\psi \to \phi \right)$$
4	2 3	syl	$$⊢\left(\forall x\in A\phi \wedge x\in A\right)\to \left(\psi \to \phi \right)$$
5	4	ex	$$⊢\forall x\in A\phi \to \left(x\in A\to \left(\psi \to \phi \right)\right)$$
6	1 5	ralrimi	$$⊢\forall x\in A\phi \to \forall x\in A\left(\psi \to \phi \right)$$