Theorem gen2 1503

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

Syntax hints:   A.wal 1400

This theorem was proved from axioms:  ax-gen 1502

This theorem is referenced by:  euequ1  2182  bm1.1  2223  vtocl3  2879  eueq  2997  csbie2  3197  moop2  4390  eusv1  4596  ordtriexmidlem  4664  ordtri2or2exmidlem  4671  onsucelsucexmidlem  4674  ordom  4752  mosubop  4839  eqrelriv  4866  opabid2  4909  xpidtr  5176  funinsn  5428  funoprab  6182  mpofun  6184  fnoprab  6185  elovmpo  6282  mpofvexi  6436  tfrlem7  6582  oaexg  6715  omexg  6718  oeiexg  6720  infiexmid  7175  domfiexmid  7176  climeu  12045  clwwlknon  16653