Theorem gen2 681

Description: Generalization applied twice.

Hypothesis

Ref	Expression
gen2.1	⊢ φ

Assertion

Ref	Expression
gen2	⊢ ∀x∀yφ

Proof of Theorem gen2

Step	Hyp	Ref	Expression
1		gen2.1	. . 3 ⊢ φ
2	1	ax-gen 677	. 2 ⊢ ∀yφ
3	2	ax-gen 677	1 ⊢ ∀x∀yφ

Syntax hints:  ∀wal 672

This theorem is referenced by:  bm1.1 1088  vtocl3 1380  eueq 1427  moop2 1910  dfrel2 2660  coi1 2665  funsn 2690  tfrlem7 2955  ster 3207  ondomon 3662  hlimeu 5146  helch 5151  hsn0elch 5155  occl 5188  chintcl 5296  osumlem7 5536

This theorem was proved from axioms:  ax-gen 677

metamath.org