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  2705  moeq  3669  csbie2  3892  mosneq  4796  eusv1  5333  moop2  5449  mosubop  5458  eqrelriv  5736  opabid2  5775  xpidtr  6075  funoprab  7475  fnoprab  7478  elovmpo  7598  tfrlem7  8312  hartogs  9455  card2on  9465  epinid0  9514  cnvepnep  9523  ssttrcl  9630  tskwe  9865  ondomon  10476  fi1uzind  14432  brfi1indALT  14435  climeu  15480  letsr  18517  ulmdm  26318  ajmoi  30820  helch  31205  hsn0elch  31210  chintcli  31293  adjmo  31794  nlelchi  32023  hmopidmchi  32113  bnj978  34918  bnj1052  34944  bnj1030  34956  funen1cnv  35057  satfv0  35333  satfv0fun  35346  fnsingle  35895  funimage  35904  funpartfun  35919  imagesset  35929  funtransport  36007  funray  36116  funline  36118  filnetlem3  36356  bj-cbvalimi  36623  bj-cbveximi  36624  ax11-pm  36808  ax11-pm2  36812  bj-snsetex  36939  wl-equsal1i  37520  mbfresfi  37648  riscer  37970  vvdifopab  38237  opabf  38338  cnvcosseq  38416  antisymressn  38423  trressn  38424  symrelcoss3  38444  cotrintab  43590  pm11.11  44350  fun2dmnopgexmpl  47272  ichv  47437  ichf  47438  ichid  47439  icht  47440  ichcircshi  47442  icheq  47450  pg4cyclnex  48115  mof0ALT  48828  f1omoOLD  48882