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  2709  moeq  3662  csbie2  3885  mosneq  4795  eusv1  5333  moop2  5447  mosubop  5456  eqrelriv  5735  opabid2  5774  xpidtr  6075  funoprab  7476  fnoprab  7479  elovmpo  7599  tfrlem7  8310  hartogs  9439  card2on  9449  epinid0  9498  cnvepnep  9507  ssttrcl  9614  tskwe  9852  ondomon  10463  fi1uzind  14418  brfi1indALT  14421  climeu  15466  letsr  18503  ulmdm  26332  ajmoi  30842  helch  31227  hsn0elch  31232  chintcli  31315  adjmo  31816  nlelchi  32045  hmopidmchi  32135  bnj978  34984  bnj1052  35010  bnj1030  35022  funen1cnv  35123  satfv0  35425  satfv0fun  35438  fnsingle  35984  funimage  35993  funpartfun  36010  imagesset  36020  funtransport  36098  funray  36207  funline  36209  filnetlem3  36447  bj-cbvalimi  36714  bj-cbveximi  36715  ax11-pm  36899  ax11-pm2  36903  bj-snsetex  37030  wl-equsal1i  37611  mbfresfi  37729  riscer  38051  vvdifopab  38320  opabf  38423  mopre  38507  cnvcosseq  38562  antisymressn  38569  trressn  38570  symrelcoss3  38590  cotrintab  43734  pm11.11  44494  fun2dmnopgexmpl  47411  ichv  47576  ichf  47577  ichid  47578  icht  47579  ichcircshi  47581  icheq  47589  pg4cyclnex  48254  mof0ALT  48967  f1omoOLD  49021