Theorem gen2 1430

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

Syntax hints:  ∀wal 1333

This theorem was proved from axioms:  ax-gen 1429

This theorem is referenced by:  euequ1  2101  bm1.1  2142  vtocl3  2768  eueq  2883  csbie2  3080  moop2  4213  eusv1  4414  ordtriexmidlem  4480  ordtri2or2exmidlem  4487  onsucelsucexmidlem  4490  ordom  4568  mosubop  4654  eqrelriv  4681  opabid2  4719  xpidtr  4978  funinsn  5221  funoprab  5923  mpofun  5925  fnoprab  5926  elovmpo  6023  mpofvexi  6156  tfrlem7  6266  oaexg  6397  omexg  6400  oeiexg  6402  infiexmid  6824  domfiexmid  6825  climeu  11204