Theorem gen2 1384

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

Syntax hints:   A.wal 1287

This theorem was proved from axioms:  ax-gen 1383

This theorem is referenced by:  euequ1  2043  bm1.1  2073  vtocl3  2675  eueq  2784  csbie2  2975  moop2  4069  eusv1  4265  ordtriexmidlem  4326  ordtri2or2exmidlem  4332  onsucelsucexmidlem  4335  ordom  4411  mosubop  4492  eqrelriv  4519  opabid2  4555  xpidtr  4809  funinsn  5049  funoprab  5727  mpt2fun  5729  fnoprab  5730  elovmpt2  5827  mpt2fvexi  5958  tfrlem7  6064  oaexg  6191  omexg  6194  oeiexg  6196  infiexmid  6573  domfiexmid  6574  climeu  10648