Theorem gen2 1461

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

Syntax hints:   A.wal 1362

This theorem was proved from axioms:  ax-gen 1460

This theorem is referenced by:  euequ1  2133  bm1.1  2174  vtocl3  2808  eueq  2923  csbie2  3121  moop2  4266  eusv1  4467  ordtriexmidlem  4533  ordtri2or2exmidlem  4540  onsucelsucexmidlem  4543  ordom  4621  mosubop  4707  eqrelriv  4734  opabid2  4773  xpidtr  5034  funinsn  5281  funoprab  5992  mpofun  5994  fnoprab  5995  elovmpo  6091  mpofvexi  6226  tfrlem7  6337  oaexg  6468  omexg  6471  oeiexg  6473  infiexmid  6900  domfiexmid  6901  climeu  11331