Theorem gen2 1498

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 1497	. 2 |- A. y ph
3	2	ax-gen 1497	1 |- A. x A. y ph

Syntax hints:   A.wal 1395

This theorem was proved from axioms:  ax-gen 1497

This theorem is referenced by:  euequ1  2174  bm1.1  2215  vtocl3  2859  eueq  2976  csbie2  3176  moop2  4346  eusv1  4551  ordtriexmidlem  4619  ordtri2or2exmidlem  4626  onsucelsucexmidlem  4629  ordom  4707  mosubop  4794  eqrelriv  4821  opabid2  4863  xpidtr  5129  funinsn  5381  funoprab  6126  mpofun  6128  fnoprab  6129  elovmpo  6226  mpofvexi  6376  tfrlem7  6488  oaexg  6621  omexg  6624  oeiexg  6626  infiexmid  7071  domfiexmid  7072  climeu  11879  clwwlknon  16309