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  4296  eusv1  4499  ordtriexmidlem  4567  ordtri2or2exmidlem  4574  onsucelsucexmidlem  4577  ordom  4655  mosubop  4741  eqrelriv  4768  opabid2  4809  xpidtr  5073  funinsn  5323  funoprab  6045  mpofun  6047  fnoprab  6048  elovmpo  6145  mpofvexi  6292  tfrlem7  6403  oaexg  6534  omexg  6537  oeiexg  6539  infiexmid  6974  domfiexmid  6975  climeu  11607