Theorem gen2 1464

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

Syntax hints:  ∀wal 1362

This theorem was proved from axioms:  ax-gen 1463

This theorem is referenced by:  euequ1  2140  bm1.1  2181  vtocl3  2820  eueq  2935  csbie2  3134  moop2  4285  eusv1  4488  ordtriexmidlem  4556  ordtri2or2exmidlem  4563  onsucelsucexmidlem  4566  ordom  4644  mosubop  4730  eqrelriv  4757  opabid2  4798  xpidtr  5061  funinsn  5308  funoprab  6026  mpofun  6028  fnoprab  6029  elovmpo  6126  mpofvexi  6268  tfrlem7  6379  oaexg  6510  omexg  6513  oeiexg  6515  infiexmid  6942  domfiexmid  6943  climeu  11466