Theorem gen2 1799

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

Syntax hints:  ∀wal 1540

This theorem was proved from axioms:  ax-gen 1798

This theorem is referenced by:  axextmo  2708  moeq  3704  csbie2  3936  mosneq  4844  eusv1  5390  moop2  5503  mosubop  5512  eqrelriv  5790  opabid2  5829  xpidtr  6124  fvmptopabOLD  7464  funoprab  7530  mpofunOLD  7533  fnoprab  7534  elovmpo  7651  wfrfunOLD  8319  tfrlem7  8383  hartogs  9539  card2on  9549  epinid0  9595  cnvepnep  9603  ssttrcl  9710  tskwe  9945  ondomon  10558  fi1uzind  14458  brfi1indALT  14461  climeu  15499  letsr  18546  ulmdm  25905  wlkResOLD  28907  ajmoi  30111  helch  30496  hsn0elch  30501  chintcli  30584  adjmo  31085  nlelchi  31314  hmopidmchi  31404  bnj978  33960  bnj1052  33986  bnj1030  33998  funen1cnv  34091  satfv0  34349  satfv0fun  34362  fnsingle  34891  funimage  34900  funpartfun  34915  imagesset  34925  funtransport  35003  funray  35112  funline  35114  filnetlem3  35265  bj-cbvalimi  35524  bj-cbveximi  35525  ax11-pm  35710  ax11-pm2  35714  bj-snsetex  35844  wl-equsal1i  36412  mbfresfi  36534  riscer  36856  vvdifopab  37128  opabf  37237  cnvcosseq  37307  antisymressn  37314  trressn  37315  symrelcoss3  37335  cotrintab  42365  pm11.11  43133  fun2dmnopgexmpl  45992  ichv  46117  ichf  46118  ichid  46119  icht  46120  ichcircshi  46122  icheq  46130  mof0ALT  47506  f1omo  47527