Theorem gen2 1438

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

Syntax hints:  ∀wal 1341

This theorem was proved from axioms:  ax-gen 1437

This theorem is referenced by:  euequ1  2109  bm1.1  2150  vtocl3  2782  eueq  2897  csbie2  3094  moop2  4229  eusv1  4430  ordtriexmidlem  4496  ordtri2or2exmidlem  4503  onsucelsucexmidlem  4506  ordom  4584  mosubop  4670  eqrelriv  4697  opabid2  4735  xpidtr  4994  funinsn  5237  funoprab  5942  mpofun  5944  fnoprab  5945  elovmpo  6039  mpofvexi  6174  tfrlem7  6285  oaexg  6416  omexg  6419  oeiexg  6421  infiexmid  6843  domfiexmid  6844  climeu  11237