Theorem gen2 1793

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

Syntax hints:  ∀wal 1535

This theorem was proved from axioms:  ax-gen 1792

This theorem is referenced by:  axextmo  2710  moeq  3716  csbie2  3950  mosneq  4847  eusv1  5397  moop2  5512  mosubop  5521  eqrelriv  5802  opabid2  5841  xpidtr  6145  fvmptopabOLD  7488  funoprab  7555  fnoprab  7558  elovmpo  7678  wfrfunOLD  8358  tfrlem7  8422  hartogs  9582  card2on  9592  epinid0  9638  cnvepnep  9646  ssttrcl  9753  tskwe  9988  ondomon  10601  fi1uzind  14543  brfi1indALT  14546  climeu  15588  letsr  18651  ulmdm  26451  wlkResOLD  29683  ajmoi  30887  helch  31272  hsn0elch  31277  chintcli  31360  adjmo  31861  nlelchi  32090  hmopidmchi  32180  bnj978  34942  bnj1052  34968  bnj1030  34980  funen1cnv  35081  satfv0  35343  satfv0fun  35356  fnsingle  35901  funimage  35910  funpartfun  35925  imagesset  35935  funtransport  36013  funray  36122  funline  36124  filnetlem3  36363  bj-cbvalimi  36630  bj-cbveximi  36631  ax11-pm  36815  ax11-pm2  36819  bj-snsetex  36946  wl-equsal1i  37525  mbfresfi  37653  riscer  37975  vvdifopab  38242  opabf  38350  cnvcosseq  38419  antisymressn  38426  trressn  38427  symrelcoss3  38447  cotrintab  43604  pm11.11  44370  fun2dmnopgexmpl  47234  ichv  47374  ichf  47375  ichid  47376  icht  47377  ichcircshi  47379  icheq  47387  mof0ALT  48670  f1omo  48691