Theorem gen2 1443

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

Syntax hints:  ∀wal 1346

This theorem was proved from axioms:  ax-gen 1442

This theorem is referenced by:  euequ1  2114  bm1.1  2155  vtocl3  2786  eueq  2901  csbie2  3098  moop2  4236  eusv1  4437  ordtriexmidlem  4503  ordtri2or2exmidlem  4510  onsucelsucexmidlem  4513  ordom  4591  mosubop  4677  eqrelriv  4704  opabid2  4742  xpidtr  5001  funinsn  5247  funoprab  5953  mpofun  5955  fnoprab  5956  elovmpo  6050  mpofvexi  6185  tfrlem7  6296  oaexg  6427  omexg  6430  oeiexg  6432  infiexmid  6855  domfiexmid  6856  climeu  11259