Theorem gen2 1473

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

Syntax hints:   A.wal 1371

This theorem was proved from axioms:  ax-gen 1472

This theorem is referenced by:  euequ1  2149  bm1.1  2190  vtocl3  2829  eueq  2944  csbie2  3143  moop2  4297  eusv1  4500  ordtriexmidlem  4568  ordtri2or2exmidlem  4575  onsucelsucexmidlem  4578  ordom  4656  mosubop  4742  eqrelriv  4769  opabid2  4810  xpidtr  5074  funinsn  5324  funoprab  6047  mpofun  6049  fnoprab  6050  elovmpo  6147  mpofvexi  6294  tfrlem7  6405  oaexg  6536  omexg  6539  oeiexg  6541  infiexmid  6976  domfiexmid  6977  climeu  11640