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  2137  bm1.1  2178  vtocl3  2817  eueq  2932  csbie2  3131  moop2  4281  eusv1  4484  ordtriexmidlem  4552  ordtri2or2exmidlem  4559  onsucelsucexmidlem  4562  ordom  4640  mosubop  4726  eqrelriv  4753  opabid2  4794  xpidtr  5057  funinsn  5304  funoprab  6019  mpofun  6021  fnoprab  6022  elovmpo  6119  mpofvexi  6261  tfrlem7  6372  oaexg  6503  omexg  6506  oeiexg  6508  infiexmid  6935  domfiexmid  6936  climeu  11442