Theorem gen2 1426

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

Syntax hints:   A.wal 1329

This theorem was proved from axioms:  ax-gen 1425

This theorem is referenced by:  euequ1  2092  bm1.1  2122  vtocl3  2737  eueq  2850  csbie2  3044  moop2  4168  eusv1  4368  ordtriexmidlem  4430  ordtri2or2exmidlem  4436  onsucelsucexmidlem  4439  ordom  4515  mosubop  4600  eqrelriv  4627  opabid2  4665  xpidtr  4924  funinsn  5167  funoprab  5864  mpofun  5866  fnoprab  5867  elovmpo  5964  mpofvexi  6097  tfrlem7  6207  oaexg  6337  omexg  6340  oeiexg  6342  infiexmid  6764  domfiexmid  6765  climeu  11058