Theorem gen2 1426

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

Syntax hints:   A.wal 1329

This theorem was proved from axioms:  ax-gen 1425

This theorem is referenced by:  euequ1  2094  bm1.1  2124  vtocl3  2742  eueq  2855  csbie2  3049  moop2  4173  eusv1  4373  ordtriexmidlem  4435  ordtri2or2exmidlem  4441  onsucelsucexmidlem  4444  ordom  4520  mosubop  4605  eqrelriv  4632  opabid2  4670  xpidtr  4929  funinsn  5172  funoprab  5871  mpofun  5873  fnoprab  5874  elovmpo  5971  mpofvexi  6104  tfrlem7  6214  oaexg  6344  omexg  6347  oeiexg  6349  infiexmid  6771  domfiexmid  6772  climeu  11065