Theorem gen2 1499

Description: Generalization applied twice. (Contributed by NM, 30-Apr-1998.)

Hypothesis

Ref	Expression
gen2.1	⊢ 𝜑

Assertion

Ref	Expression
gen2	⊢ ∀𝑥∀𝑦𝜑

Proof of Theorem gen2

Step	Hyp	Ref	Expression
1		gen2.1	. . 3 ⊢ 𝜑
2	1	ax-gen 1498	. 2 ⊢ ∀𝑦𝜑
3	2	ax-gen 1498	1 ⊢ ∀𝑥∀𝑦𝜑

Syntax hints:  ∀wal 1396

This theorem was proved from axioms:  ax-gen 1498

This theorem is referenced by:  euequ1  2175  bm1.1  2216  vtocl3  2861  eueq  2978  csbie2  3178  moop2  4350  eusv1  4555  ordtriexmidlem  4623  ordtri2or2exmidlem  4630  onsucelsucexmidlem  4633  ordom  4711  mosubop  4798  eqrelriv  4825  opabid2  4867  xpidtr  5134  funinsn  5386  funoprab  6131  mpofun  6133  fnoprab  6134  elovmpo  6231  mpofvexi  6380  tfrlem7  6526  oaexg  6659  omexg  6662  oeiexg  6664  infiexmid  7109  domfiexmid  7110  climeu  11919  clwwlknon  16353