Theorem gen2 1461

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 1460	. 2 ⊢ ∀𝑦𝜑
3	2	ax-gen 1460	1 ⊢ ∀𝑥∀𝑦𝜑

Syntax hints:  ∀wal 1362

This theorem was proved from axioms:  ax-gen 1460

This theorem is referenced by:  euequ1  2133  bm1.1  2174  vtocl3  2808  eueq  2923  csbie2  3121  moop2  4272  eusv1  4473  ordtriexmidlem  4539  ordtri2or2exmidlem  4546  onsucelsucexmidlem  4549  ordom  4627  mosubop  4713  eqrelriv  4740  opabid2  4779  xpidtr  5040  funinsn  5287  funoprab  6000  mpofun  6002  fnoprab  6003  elovmpo  6099  mpofvexi  6235  tfrlem7  6346  oaexg  6477  omexg  6480  oeiexg  6482  infiexmid  6909  domfiexmid  6910  climeu  11345