Theorem gen2 1496

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

Syntax hints:   A.wal 1393

This theorem was proved from axioms:  ax-gen 1495

This theorem is referenced by:  euequ1  2173  bm1.1  2214  vtocl3  2857  eueq  2974  csbie2  3174  moop2  4338  eusv1  4543  ordtriexmidlem  4611  ordtri2or2exmidlem  4618  onsucelsucexmidlem  4621  ordom  4699  mosubop  4785  eqrelriv  4812  opabid2  4853  xpidtr  5119  funinsn  5370  funoprab  6104  mpofun  6106  fnoprab  6107  elovmpo  6204  mpofvexi  6352  tfrlem7  6463  oaexg  6594  omexg  6597  oeiexg  6599  infiexmid  7039  domfiexmid  7040  climeu  11807