Theorem ralimda

Description: Deduction quantifying both antecedent and consequent. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	ralimda.1	⊢ Ⅎ 𝑥 𝜑
	ralimda.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝜓 → 𝜒 ) )
Assertion	ralimda	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐴 𝜓 → ∀ 𝑥 ∈ 𝐴 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		ralimda.1	⊢ Ⅎ 𝑥 𝜑
2		ralimda.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝜓 → 𝜒 ) )
3		nfra1	⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ 𝐴 𝜓
4	1 3	nfan	⊢ Ⅎ 𝑥 ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 )
5		id	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) )
6	5	adantlr	⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) )
7		rspa	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝜓 ∧ 𝑥 ∈ 𝐴 ) → 𝜓 )
8	7	adantll	⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) ∧ 𝑥 ∈ 𝐴 ) → 𝜓 )
9	6 8 2	sylc	⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) ∧ 𝑥 ∈ 𝐴 ) → 𝜒 )
10	4 9	ralrimia	⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) → ∀ 𝑥 ∈ 𝐴 𝜒 )
11	10	ex	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐴 𝜓 → ∀ 𝑥 ∈ 𝐴 𝜒 ) )