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 ⊢ ∀𝑥∀𝑦𝜑

Syntax hints:  ∀wal 1400

This theorem was proved from axioms:  ax-gen 1502

This theorem is referenced by:  euequ1  2182  bm1.1  2223  vtocl3  2879  eueq  2997  csbie2  3197  moop2  4387  eusv1  4593  ordtriexmidlem  4661  ordtri2or2exmidlem  4668  onsucelsucexmidlem  4671  ordom  4749  mosubop  4836  eqrelriv  4863  opabid2  4906  xpidtr  5173  funinsn  5425  funoprab  6178  mpofun  6180  fnoprab  6181  elovmpo  6278  mpofvexi  6432  tfrlem7  6578  oaexg  6711  omexg  6714  oeiexg  6716  infiexmid  7171  domfiexmid  7172  climeu  12040  clwwlknon  16584