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  2176  bm1.1  2217  vtocl3  2871  eueq  2988  csbie2  3188  moop2  4368  eusv1  4573  ordtriexmidlem  4641  ordtri2or2exmidlem  4648  onsucelsucexmidlem  4651  ordom  4729  mosubop  4816  eqrelriv  4843  opabid2  4886  xpidtr  5153  funinsn  5405  funoprab  6153  mpofun  6155  fnoprab  6156  elovmpo  6253  mpofvexi  6402  tfrlem7  6548  oaexg  6681  omexg  6684  oeiexg  6686  infiexmid  7134  domfiexmid  7135  climeu  11981  clwwlknon  16424