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  2176  bm1.1  2217  vtocl3  2870  eueq  2987  csbie2  3187  moop2  4367  eusv1  4572  ordtriexmidlem  4640  ordtri2or2exmidlem  4647  onsucelsucexmidlem  4650  ordom  4728  mosubop  4815  eqrelriv  4842  opabid2  4885  xpidtr  5152  funinsn  5404  funoprab  6152  mpofun  6154  fnoprab  6155  elovmpo  6252  mpofvexi  6401  tfrlem7  6547  oaexg  6680  omexg  6683  oeiexg  6685  infiexmid  7133  domfiexmid  7134  climeu  11974  clwwlknon  16411