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  2175  bm1.1  2216  vtocl3  2860  eueq  2977  csbie2  3177  moop2  4344  eusv1  4549  ordtriexmidlem  4617  ordtri2or2exmidlem  4624  onsucelsucexmidlem  4627  ordom  4705  mosubop  4792  eqrelriv  4819  opabid2  4861  xpidtr  5127  funinsn  5379  funoprab  6121  mpofun  6123  fnoprab  6124  elovmpo  6221  mpofvexi  6371  tfrlem7  6483  oaexg  6616  omexg  6619  oeiexg  6621  infiexmid  7066  domfiexmid  7067  climeu  11858  clwwlknon  16283