Theorem gen2 1797

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

Syntax hints:  ∀wal 1539

This theorem was proved from axioms:  ax-gen 1796

This theorem is referenced by:  axextmo  2712  moeq  3665  csbie2  3888  mosneq  4798  eusv1  5336  moop2  5450  mosubop  5459  eqrelriv  5738  opabid2  5777  xpidtr  6079  funoprab  7480  fnoprab  7483  elovmpo  7603  tfrlem7  8314  hartogs  9449  card2on  9459  epinid0  9508  cnvepnep  9517  ssttrcl  9624  tskwe  9862  ondomon  10473  fi1uzind  14430  brfi1indALT  14433  climeu  15478  letsr  18516  ulmdm  26358  ajmoi  30933  helch  31318  hsn0elch  31323  chintcli  31406  adjmo  31907  nlelchi  32136  hmopidmchi  32226  bnj978  35105  bnj1052  35131  bnj1030  35143  funen1cnv  35244  satfv0  35552  satfv0fun  35565  fnsingle  36111  funimage  36120  funpartfun  36137  imagesset  36147  funtransport  36225  funray  36334  funline  36336  filnetlem3  36574  bj-cbvalimi  36847  bj-cbveximi  36848  ax11-pm  37033  ax11-pm2  37037  bj-snsetex  37164  wl-equsal1i  37749  mbfresfi  37867  riscer  38189  vvdifopab  38458  opabf  38561  mopre  38645  cnvcosseq  38700  antisymressn  38707  trressn  38708  symrelcoss3  38728  cotrintab  43855  pm11.11  44615  fun2dmnopgexmpl  47530  ichv  47695  ichf  47696  ichid  47697  icht  47698  ichcircshi  47700  icheq  47708  pg4cyclnex  48373  mof0ALT  49085  f1omoOLD  49139