Theorem gen2 1496

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

Syntax hints:  ∀wal 1393

This theorem was proved from axioms:  ax-gen 1495

This theorem is referenced by:  euequ1  2173  bm1.1  2214  vtocl3  2858  eueq  2975  csbie2  3175  moop2  4342  eusv1  4547  ordtriexmidlem  4615  ordtri2or2exmidlem  4622  onsucelsucexmidlem  4625  ordom  4703  mosubop  4790  eqrelriv  4817  opabid2  4859  xpidtr  5125  funinsn  5376  funoprab  6116  mpofun  6118  fnoprab  6119  elovmpo  6216  mpofvexi  6366  tfrlem7  6478  oaexg  6611  omexg  6614  oeiexg  6616  infiexmid  7059  domfiexmid  7060  climeu  11847  clwwlknon  16224