Theorem gen2 1379

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

Syntax hints:   A.wal 1282

This theorem was proved from axioms:  ax-gen 1378

This theorem is referenced by:  euequ1  2036  bm1.1  2066  vtocl3  2655  eueq  2763  csbie2  2951  moop2  4006  eusv1  4202  ordtriexmidlem  4263  ordtri2or2exmidlem  4269  onsucelsucexmidlem  4272  ordom  4347  mosubop  4424  eqrelriv  4451  opabid2  4485  xpidtr  4735  funoprab  5621  mpt2fun  5623  fnoprab  5624  elovmpt2  5721  mpt2fvexi  5852  tfrlem7  5956  oaexg  6051  omexg  6054  oeiexg  6056  infiexmid  6362  domfiexmid  6363  climeu  10135