This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ∀ 𝑥 ∀ 𝑦 𝜑