Theorem gen2 1796

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

Syntax hints:  ∀wal 1538

This theorem was proved from axioms:  ax-gen 1795

This theorem is referenced by:  axextmo  2712  moeq  3695  csbie2  3918  mosneq  4823  eusv1  5366  moop2  5482  mosubop  5491  eqrelriv  5773  opabid2  5812  xpidtr  6116  fvmptopabOLD  7467  funoprab  7534  fnoprab  7537  elovmpo  7657  wfrfunOLD  8338  tfrlem7  8402  hartogs  9563  card2on  9573  epinid0  9619  cnvepnep  9627  ssttrcl  9734  tskwe  9969  ondomon  10582  fi1uzind  14530  brfi1indALT  14533  climeu  15576  letsr  18608  ulmdm  26359  wlkResOLD  29635  ajmoi  30844  helch  31229  hsn0elch  31234  chintcli  31317  adjmo  31818  nlelchi  32047  hmopidmchi  32137  bnj978  34985  bnj1052  35011  bnj1030  35023  funen1cnv  35124  satfv0  35385  satfv0fun  35398  fnsingle  35942  funimage  35951  funpartfun  35966  imagesset  35976  funtransport  36054  funray  36163  funline  36165  filnetlem3  36403  bj-cbvalimi  36670  bj-cbveximi  36671  ax11-pm  36855  ax11-pm2  36859  bj-snsetex  36986  wl-equsal1i  37567  mbfresfi  37695  riscer  38017  vvdifopab  38283  opabf  38391  cnvcosseq  38460  antisymressn  38467  trressn  38468  symrelcoss3  38488  cotrintab  43605  pm11.11  44365  fun2dmnopgexmpl  47280  ichv  47430  ichf  47431  ichid  47432  icht  47433  ichcircshi  47435  icheq  47443  mof0ALT  48785  f1omo  48835