Theorem gen2 1407

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

Syntax hints:  ∀wal 1310

This theorem was proved from axioms:  ax-gen 1406

This theorem is referenced by:  euequ1  2068  bm1.1  2098  vtocl3  2711  eueq  2822  csbie2  3013  moop2  4131  eusv1  4331  ordtriexmidlem  4393  ordtri2or2exmidlem  4399  onsucelsucexmidlem  4402  ordom  4478  mosubop  4563  eqrelriv  4590  opabid2  4628  xpidtr  4885  funinsn  5128  funoprab  5823  mpofun  5825  fnoprab  5826  elovmpo  5923  mpofvexi  6055  tfrlem7  6165  oaexg  6295  omexg  6298  oeiexg  6300  infiexmid  6721  domfiexmid  6722  climeu  10950