Theorem gen2 1499

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

Syntax hints:  ∀wal 1396

This theorem was proved from axioms:  ax-gen 1498

This theorem is referenced by:  euequ1  2178  bm1.1  2219  vtocl3  2873  eueq  2991  csbie2  3191  moop2  4373  eusv1  4578  ordtriexmidlem  4646  ordtri2or2exmidlem  4653  onsucelsucexmidlem  4656  ordom  4734  mosubop  4821  eqrelriv  4848  opabid2  4891  xpidtr  5158  funinsn  5410  funoprab  6161  mpofun  6163  fnoprab  6164  elovmpo  6261  mpofvexi  6415  tfrlem7  6561  oaexg  6694  omexg  6697  oeiexg  6699  infiexmid  7147  domfiexmid  7148  climeu  12006  clwwlknon  16550