Theorem gen2 1464

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

Syntax hints:   A.wal 1362

This theorem was proved from axioms:  ax-gen 1463

This theorem is referenced by:  euequ1  2140  bm1.1  2181  vtocl3  2820  eueq  2935  csbie2  3134  moop2  4284  eusv1  4487  ordtriexmidlem  4555  ordtri2or2exmidlem  4562  onsucelsucexmidlem  4565  ordom  4643  mosubop  4729  eqrelriv  4756  opabid2  4797  xpidtr  5060  funinsn  5307  funoprab  6022  mpofun  6024  fnoprab  6025  elovmpo  6122  mpofvexi  6264  tfrlem7  6375  oaexg  6506  omexg  6509  oeiexg  6511  infiexmid  6938  domfiexmid  6939  climeu  11461