Theorem gen2 1498

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

Syntax hints:  ∀wal 1395

This theorem was proved from axioms:  ax-gen 1497

This theorem is referenced by:  euequ1  2175  bm1.1  2216  vtocl3  2860  eueq  2977  csbie2  3177  moop2  4344  eusv1  4549  ordtriexmidlem  4617  ordtri2or2exmidlem  4624  onsucelsucexmidlem  4627  ordom  4705  mosubop  4792  eqrelriv  4819  opabid2  4861  xpidtr  5127  funinsn  5379  funoprab  6120  mpofun  6122  fnoprab  6123  elovmpo  6220  mpofvexi  6370  tfrlem7  6482  oaexg  6615  omexg  6618  oeiexg  6620  infiexmid  7065  domfiexmid  7066  climeu  11856  clwwlknon  16279