Theorem gen2 1503

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

This proof depends on syntax axioms:  ∀wal 1400

This proof depends on axioms:  ax-gen 1502

This theorem is used by:  euequ1  2182  bm1.1  2223  vtocl3  2879  eueq  2997  csbie2  3197  moop2  4394  eusv1  4600  ordtriexmidlem  4668  ordtri2or2exmidlem  4675  onsucelsucexmidlem  4678  ordom  4756  mosubop  4843  eqrelriv  4870  opabid2  4913  xpidtr  5181  funinsn  5433  funoprab  6191  mpofun  6193  fnoprab  6194  elovmpo  6291  mpofvexi  6446  tfrlem7  6592  oaexg  6725  omexg  6728  oeiexg  6730  infiexmid  7185  domfiexmid  7186  climeu  12087  clwwlknon  16875