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  3703  csbie2  3935  mosneq  4843  eusv1  5389  moop2  5502  mosubop  5511  eqrelriv  5788  opabid2  5827  xpidtr  6121  fvmptopabOLD  7461  funoprab  7527  mpofunOLD  7530  fnoprab  7531  elovmpo  7648  wfrfunOLD  8316  tfrlem7  8380  hartogs  9536  card2on  9546  epinid0  9592  cnvepnep  9600  ssttrcl  9707  tskwe  9942  ondomon  10555  fi1uzind  14455  brfi1indALT  14458  climeu  15496  letsr  18543  ulmdm  25897  wlkResOLD  28897  ajmoi  30099  helch  30484  hsn0elch  30489  chintcli  30572  adjmo  31073  nlelchi  31302  hmopidmchi  31392  bnj978  33949  bnj1052  33975  bnj1030  33987  funen1cnv  34080  satfv0  34338  satfv0fun  34351  fnsingle  34880  funimage  34889  funpartfun  34904  imagesset  34914  funtransport  34992  funray  35101  funline  35103  filnetlem3  35254  bj-cbvalimi  35513  bj-cbveximi  35514  ax11-pm  35699  ax11-pm2  35703  bj-snsetex  35833  wl-equsal1i  36401  mbfresfi  36523  riscer  36845  vvdifopab  37117  opabf  37226  cnvcosseq  37296  antisymressn  37303  trressn  37304  symrelcoss3  37324  cotrintab  42351  pm11.11  43119  fun2dmnopgexmpl  45979  ichv  46104  ichf  46105  ichid  46106  icht  46107  ichcircshi  46109  icheq  46117  mof0ALT  47460  f1omo  47481