Theorem gen2 1547

Description: Generalization applied twice. (Contributed by NM, 30-Apr-1998.)

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

Syntax hints:  ∀wal 1540

This theorem was proved from axioms:  ax-gen 1546

This theorem is referenced by:  euequ1  2292  bm1.1  2338  vtocl3  2912  eueq  3009  csbie2  3182  eqrelkriiv  4214  sikss1c1c  4268  ins2kss  4280  ins3kss  4281  nnsucelr  4429  ssfin  4471  ncfinlower  4484  mosubop  4614  eqoprriv  4854  fvopab4t  5386  1stfo  5506  2ndfo  5507  swapf1o  5512  funoprab  5585  fnoprab  5587  fnfullfunlem2  5858  fvfullfunlem2  5863  fvfullfunlem3  5864  xpassen  6058