Theorem gen2 1499

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

Hypothesis

Ref	Expression
gen2.1	|- ph

Assertion

Ref	Expression
gen2	|- A. x A. y ph

Proof of Theorem gen2

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

Syntax hints:   A.wal 1396

This theorem was proved from axioms:  ax-gen 1498

This theorem is referenced by:  euequ1  2178  bm1.1  2219  vtocl3  2873  eueq  2990  csbie2  3190  moop2  4370  eusv1  4575  ordtriexmidlem  4643  ordtri2or2exmidlem  4650  onsucelsucexmidlem  4653  ordom  4731  mosubop  4818  eqrelriv  4845  opabid2  4888  xpidtr  5155  funinsn  5407  funoprab  6155  mpofun  6157  fnoprab  6158  elovmpo  6255  mpofvexi  6404  tfrlem7  6550  oaexg  6683  omexg  6686  oeiexg  6688  infiexmid  7136  domfiexmid  7137  climeu  11989  clwwlknon  16473