Theorem gen2 1791

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

Syntax hints:  ∀wal 1532

This theorem was proved from axioms:  ax-gen 1790

This theorem is referenced by:  axextmo  2701  moeq  3700  csbie2  3933  mosneq  4841  eusv1  5387  moop2  5500  mosubop  5509  eqrelriv  5787  opabid2  5826  xpidtr  6126  fvmptopabOLD  7472  funoprab  7539  mpofunOLD  7542  fnoprab  7543  elovmpo  7663  wfrfunOLD  8341  tfrlem7  8405  hartogs  9580  card2on  9590  epinid0  9636  cnvepnep  9644  ssttrcl  9751  tskwe  9986  ondomon  10597  fi1uzind  14511  brfi1indALT  14514  climeu  15552  letsr  18613  ulmdm  26419  wlkResOLD  29584  ajmoi  30788  helch  31173  hsn0elch  31178  chintcli  31261  adjmo  31762  nlelchi  31991  hmopidmchi  32081  bnj978  34807  bnj1052  34833  bnj1030  34845  funen1cnv  34938  satfv0  35199  satfv0fun  35212  fnsingle  35756  funimage  35765  funpartfun  35780  imagesset  35790  funtransport  35868  funray  35977  funline  35979  filnetlem3  36105  bj-cbvalimi  36364  bj-cbveximi  36365  ax11-pm  36550  ax11-pm2  36554  bj-snsetex  36683  wl-equsal1i  37252  mbfresfi  37380  riscer  37702  vvdifopab  37971  opabf  38079  cnvcosseq  38148  antisymressn  38155  trressn  38156  symrelcoss3  38176  cotrintab  43318  pm11.11  44085  fun2dmnopgexmpl  46933  ichv  47057  ichf  47058  ichid  47059  icht  47060  ichcircshi  47062  icheq  47070  mof0ALT  48243  f1omo  48264