Theorem gen2 1794

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

Syntax hints:  ∀wal 1535

This theorem was proved from axioms:  ax-gen 1793

This theorem is referenced by:  axextmo  2715  moeq  3729  csbie2  3963  mosneq  4867  eusv1  5409  moop2  5521  mosubop  5530  eqrelriv  5813  opabid2  5852  xpidtr  6154  fvmptopabOLD  7505  funoprab  7572  fnoprab  7575  elovmpo  7695  wfrfunOLD  8375  tfrlem7  8439  hartogs  9613  card2on  9623  epinid0  9669  cnvepnep  9677  ssttrcl  9784  tskwe  10019  ondomon  10632  fi1uzind  14556  brfi1indALT  14559  climeu  15601  letsr  18663  ulmdm  26454  wlkResOLD  29686  ajmoi  30890  helch  31275  hsn0elch  31280  chintcli  31363  adjmo  31864  nlelchi  32093  hmopidmchi  32183  bnj978  34925  bnj1052  34951  bnj1030  34963  funen1cnv  35064  satfv0  35326  satfv0fun  35339  fnsingle  35883  funimage  35892  funpartfun  35907  imagesset  35917  funtransport  35995  funray  36104  funline  36106  filnetlem3  36346  bj-cbvalimi  36613  bj-cbveximi  36614  ax11-pm  36798  ax11-pm2  36802  bj-snsetex  36929  wl-equsal1i  37498  mbfresfi  37626  riscer  37948  vvdifopab  38216  opabf  38324  cnvcosseq  38393  antisymressn  38400  trressn  38401  symrelcoss3  38421  cotrintab  43576  pm11.11  44343  fun2dmnopgexmpl  47199  ichv  47323  ichf  47324  ichid  47325  icht  47326  ichcircshi  47328  icheq  47336  mof0ALT  48553  f1omo  48574