Metamath Proof Explorer


Theorem gen2

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

Ref Expression
Hypothesis gen2.1
|- ph
Assertion gen2
|- A. x A. y ph

Proof

Step Hyp Ref Expression
1 gen2.1
 |-  ph
2 1 ax-gen
 |-  A. y ph
3 2 ax-gen
 |-  A. x A. y ph