Theorem gen2 1430

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

Syntax hints:   A.wal 1333

This theorem was proved from axioms:  ax-gen 1429

This theorem is referenced by:  euequ1  2101  bm1.1  2142  vtocl3  2768  eueq  2883  csbie2  3080  moop2  4211  eusv1  4411  ordtriexmidlem  4477  ordtri2or2exmidlem  4484  onsucelsucexmidlem  4487  ordom  4565  mosubop  4651  eqrelriv  4678  opabid2  4716  xpidtr  4975  funinsn  5218  funoprab  5918  mpofun  5920  fnoprab  5921  elovmpo  6018  mpofvexi  6151  tfrlem7  6261  oaexg  6392  omexg  6395  oeiexg  6397  infiexmid  6819  domfiexmid  6820  climeu  11186