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 1537

This theorem was proved from axioms:  ax-gen 1795

This theorem is referenced by:  axextmo  2711  moeq  3647  csbie2  3879  mosneq  4779  eusv1  5323  moop2  5429  mosubop  5438  eqrelriv  5711  opabid2  5750  xpidtr  6042  fvmptopabOLD  7362  funoprab  7428  mpofunOLD  7431  fnoprab  7432  elovmpo  7546  wfrfunOLD  8181  tfrlem7  8245  hartogs  9351  card2on  9361  epinid0  9407  cnvepnep  9414  ssttrcl  9521  tskwe  9756  ondomon  10369  fi1uzind  14260  brfi1indALT  14263  climeu  15313  letsr  18360  ulmdm  25601  wlkResOLD  28066  ajmoi  29269  helch  29654  hsn0elch  29659  chintcli  29742  adjmo  30243  nlelchi  30472  hmopidmchi  30562  bnj978  32978  bnj1052  33004  bnj1030  33016  funen1cnv  33109  satfv0  33369  satfv0fun  33382  fnsingle  34270  funimage  34279  funpartfun  34294  imagesset  34304  funtransport  34382  funray  34491  funline  34493  filnetlem3  34618  bj-cbvalimi  34877  bj-cbveximi  34878  ax11-pm  35063  ax11-pm2  35067  bj-snsetex  35201  wl-equsal1i  35750  mbfresfi  35871  riscer  36194  vvdifopab  36470  opabf  36581  cnvcosseq  36651  antisymressn  36658  trressn  36659  symrelcoss3  36679  cotrintab  41435  pm11.11  42205  fun2dmnopgexmpl  45020  ichv  45145  ichf  45146  ichid  45147  icht  45148  ichcircshi  45150  icheq  45158  mof0ALT  46411  f1omo  46432