Theorem gen2

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

	Ref	Expression
Hypothesis	gen2.1	⊢ 𝜑
Assertion	gen2	⊢ ∀ 𝑥 ∀ 𝑦 𝜑

Proof

Step	Hyp	Ref	Expression
1		gen2.1	⊢ 𝜑
2	1	ax-gen	⊢ ∀ 𝑦 𝜑
3	2	ax-gen	⊢ ∀ 𝑥 ∀ 𝑦 𝜑