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  6273  tfrlem7  6384  oaexg  6515  omexg  6518  oeiexg  6520  infiexmid  6947  domfiexmid  6948  climeu  11478