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  3678  csbie2  3901  mosneq  4806  eusv1  5346  moop2  5462  mosubop  5471  eqrelriv  5752  opabid2  5791  xpidtr  6095  fvmptopabOLD  7444  funoprab  7511  fnoprab  7514  elovmpo  7634  tfrlem7  8351  hartogs  9497  card2on  9507  epinid0  9553  cnvepnep  9561  ssttrcl  9668  tskwe  9903  ondomon  10516  fi1uzind  14472  brfi1indALT  14475  climeu  15521  letsr  18552  ulmdm  26302  wlkResOLD  29578  ajmoi  30787  helch  31172  hsn0elch  31177  chintcli  31260  adjmo  31761  nlelchi  31990  hmopidmchi  32080  bnj978  34939  bnj1052  34965  bnj1030  34977  funen1cnv  35078  satfv0  35345  satfv0fun  35358  fnsingle  35907  funimage  35916  funpartfun  35931  imagesset  35941  funtransport  36019  funray  36128  funline  36130  filnetlem3  36368  bj-cbvalimi  36635  bj-cbveximi  36636  ax11-pm  36820  ax11-pm2  36824  bj-snsetex  36951  wl-equsal1i  37532  mbfresfi  37660  riscer  37982  vvdifopab  38249  opabf  38350  cnvcosseq  38428  antisymressn  38435  trressn  38436  symrelcoss3  38456  cotrintab  43603  pm11.11  44363  fun2dmnopgexmpl  47282  ichv  47447  ichf  47448  ichid  47449  icht  47450  ichcircshi  47452  icheq  47460  pg4cyclnex  48114  mof0ALT  48825  f1omoOLD  48879