Theorem gen2

Description: Generalization applied twice. (Contributed by NM, 30-Apr-1998)

	Ref	Expression
Hypothesis	gen2.1	$$⊢\phi$$
Assertion	gen2	$$⊢\forall x\forall y\phi$$

Proof

Step	Hyp	Ref	Expression
1		gen2.1	$$⊢\phi$$
2	1	ax-gen	$$⊢\forall y\phi$$
3	2	ax-gen	$$⊢\forall x\forall y\phi$$