This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 φ \to \forall x \in A (ψ \to φ)$

Step	Hyp	Ref	Expression
1		nfra1	$⊢ Ⅎ x \forall x \in A φ$
2		rspa	$⊢ (\forall x \in A φ \land x \in A) \to φ$
3		ax-1	$⊢ φ \to (ψ \to φ)$
4	2 3	syl	$⊢ (\forall x \in A φ \land x \in A) \to (ψ \to φ)$
5	4	ex	$⊢ \forall x \in A φ \to (x \in A \to (ψ \to φ))$
6	1 5	ralrimi	$⊢ \forall x \in A φ \to \forall x \in A (ψ \to φ)$