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  2707  moeq  3666  csbie2  3889  mosneq  4794  eusv1  5329  moop2  5442  mosubop  5451  eqrelriv  5729  opabid2  5768  xpidtr  6069  funoprab  7468  fnoprab  7471  elovmpo  7591  tfrlem7  8302  hartogs  9430  card2on  9440  epinid0  9489  cnvepnep  9498  ssttrcl  9605  tskwe  9843  ondomon  10454  fi1uzind  14414  brfi1indALT  14417  climeu  15462  letsr  18499  ulmdm  26330  ajmoi  30836  helch  31221  hsn0elch  31226  chintcli  31309  adjmo  31810  nlelchi  32039  hmopidmchi  32129  bnj978  34959  bnj1052  34985  bnj1030  34997  funen1cnv  35098  satfv0  35400  satfv0fun  35413  fnsingle  35959  funimage  35968  funpartfun  35983  imagesset  35993  funtransport  36071  funray  36180  funline  36182  filnetlem3  36420  bj-cbvalimi  36687  bj-cbveximi  36688  ax11-pm  36872  ax11-pm2  36876  bj-snsetex  37003  wl-equsal1i  37584  mbfresfi  37712  riscer  38034  vvdifopab  38301  opabf  38402  cnvcosseq  38480  antisymressn  38487  trressn  38488  symrelcoss3  38508  cotrintab  43653  pm11.11  44413  fun2dmnopgexmpl  47321  ichv  47486  ichf  47487  ichid  47488  icht  47489  ichcircshi  47491  icheq  47499  pg4cyclnex  48164  mof0ALT  48877  f1omoOLD  48931