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  2137  bm1.1  2178  vtocl3  2816  eueq  2931  csbie2  3130  moop2  4280  eusv1  4483  ordtriexmidlem  4551  ordtri2or2exmidlem  4558  onsucelsucexmidlem  4561  ordom  4639  mosubop  4725  eqrelriv  4752  opabid2  4793  xpidtr  5056  funinsn  5303  funoprab  6018  mpofun  6020  fnoprab  6021  elovmpo  6117  mpofvexi  6259  tfrlem7  6370  oaexg  6501  omexg  6504  oeiexg  6506  infiexmid  6933  domfiexmid  6934  climeu  11439