Theorem 2alimi

Description: Inference doubly quantifying both antecedent and consequent. (Contributed by NM, 3-Feb-2005)

	Ref	Expression
Hypothesis	alimi.1	$$⊢\phi \to \psi$$
Assertion	2alimi	$$⊢\forall x\forall y\phi \to \forall x\forall y\psi$$

Proof

Step	Hyp	Ref	Expression
1		alimi.1	$$⊢\phi \to \psi$$
2	1	alimi	$$⊢\forall y\phi \to \forall y\psi$$
3	2	alimi	$$⊢\forall x\forall y\phi \to \forall x\forall y\psi$$