Theorem gen2 981

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 961	. 2 ⊢ ∀yφ
3	2	ax-gen 961	1 ⊢ ∀x∀yφ

Syntax hints:  ∀wal 952

This theorem is referenced by:  bm1.1 1460  vtocl3 1840  eueq 1912  csbie2 2030  csbco3g 2036  sbcco3g 2037  moop2 2796  mosubop 2800  opabid2 3262  dfrel2 3477  coi1 3502  funsn 3535  tfrlem7 3908  funoprab 4002  fnoprab 4004  ster 4258  ondomon 4836  climeu 7045  ajmoi 8463  hlimeu 9050  helch 9055  hsn0elch 9059  occl 9120  chintcl 9233  osumlem7 9524  adjmo 9698  nlelch 9932  bra11 9979  hmopidmch 10017  fgsb 10480  fgsb2 10485

This theorem was proved from axioms:  ax-gen 961

Copyright terms: Public domain