Theorem gen2 1339

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

Syntax hints:  ∀wal 1241

This theorem was proved from axioms:  ax-gen 1338

This theorem is referenced by:  euequ1  1995  bm1.1  2025  vtocl3  2610  eueq  2712  csbie2  2895  moop2  3988  eusv1  4184  ordtriexmidlem  4245  ordtri2or2exmidlem  4251  onsucelsucexmidlem  4254  ordom  4329  mosubop  4406  eqrelriv  4433  opabid2  4467  xpidtr  4715  funoprab  5601  mpt2fun  5603  fnoprab  5604  elovmpt2  5701  mpt2fvexi  5832  tfrlem7  5933  oaexg  6028  omexg  6031  oeiexg  6033  climeu  9817