Theorem gen2 1474

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

Syntax hints:   A.wal 1371

This theorem was proved from axioms:  ax-gen 1473

This theorem is referenced by:  euequ1  2151  bm1.1  2192  vtocl3  2834  eueq  2951  csbie2  3151  moop2  4314  eusv1  4517  ordtriexmidlem  4585  ordtri2or2exmidlem  4592  onsucelsucexmidlem  4595  ordom  4673  mosubop  4759  eqrelriv  4786  opabid2  4827  xpidtr  5092  funinsn  5342  funoprab  6068  mpofun  6070  fnoprab  6071  elovmpo  6168  mpofvexi  6315  tfrlem7  6426  oaexg  6557  omexg  6560  oeiexg  6562  infiexmid  7000  domfiexmid  7001  climeu  11722