Theorem ralimralim

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

	Ref	Expression
Assertion	ralimralim	⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 → ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		nfra1	⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ 𝐴 𝜑
2		rspa	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝜑 )
3		ax-1	⊢ ( 𝜑 → ( 𝜓 → 𝜑 ) )
4	2 3	syl	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝜓 → 𝜑 ) )
5	4	ex	⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 → ( 𝑥 ∈ 𝐴 → ( 𝜓 → 𝜑 ) ) )
6	1 5	ralrimi	⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 → ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜑 ) )