Theorem ralimda

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

	Ref	Expression
Hypotheses	ralimda.1	$$⊢Ⅎx\phi$$
	ralimda.2	$$⊢\left(\phi \wedge x\in A\right)\to \left(\psi \to \chi \right)$$
Assertion	ralimda	$$⊢\phi \to \left(\forall x\in A\psi \to \forall x\in A\chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		ralimda.1	$$⊢Ⅎx\phi$$
2		ralimda.2	$$⊢\left(\phi \wedge x\in A\right)\to \left(\psi \to \chi \right)$$
3		nfra1	$$⊢Ⅎx\forall x\in A\psi$$
4	1 3	nfan	$$⊢Ⅎx\left(\phi \wedge \forall x\in A\psi \right)$$
5		id	$$⊢\left(\phi \wedge x\in A\right)\to \left(\phi \wedge x\in A\right)$$
6	5	adantlr	$$⊢\left(\left(\phi \wedge \forall x\in A\psi \right)\wedge x\in A\right)\to \left(\phi \wedge x\in A\right)$$
7		rspa	$$⊢\left(\forall x\in A\psi \wedge x\in A\right)\to \psi$$
8	7	adantll	$$⊢\left(\left(\phi \wedge \forall x\in A\psi \right)\wedge x\in A\right)\to \psi$$
9	6 8 2	sylc	$$⊢\left(\left(\phi \wedge \forall x\in A\psi \right)\wedge x\in A\right)\to \chi$$
10	4 9	ralrimia	$$⊢\left(\phi \wedge \forall x\in A\psi \right)\to \forall x\in A\chi$$
11	10	ex	$$⊢\phi \to \left(\forall x\in A\psi \to \forall x\in A\chi \right)$$