Theorem gen2 1798

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

Syntax hints:  ∀wal 1536

This theorem was proved from axioms:  ax-gen 1797

This theorem is referenced by:  axextmo  2733  moeq  3621  csbie2  3844  mosneq  4730  eusv1  5260  moop2  5361  mosubop  5370  eqrelriv  5631  opabid2  5669  xpidtr  5954  fvmptopab  7203  funoprab  7268  mpofunOLD  7271  fnoprab  7272  elovmpo  7386  wfrfun  7975  tfrlem7  8029  hartogs  9041  card2on  9051  epinid0  9097  cnvepnep  9104  tskwe  9412  ondomon  10023  fi1uzind  13907  brfi1indALT  13910  climeu  14960  letsr  17903  ulmdm  25087  wlkRes  27538  ajmoi  28740  helch  29125  hsn0elch  29130  chintcli  29213  adjmo  29714  nlelchi  29943  hmopidmchi  30033  bnj978  32449  bnj1052  32475  bnj1030  32487  funen1cnv  32585  satfv0  32836  satfv0fun  32849  fnsingle  33792  funimage  33801  funpartfun  33816  imagesset  33826  funtransport  33904  funray  34013  funline  34015  filnetlem3  34140  bj-cbvalimi  34396  bj-cbveximi  34397  ax11-pm  34573  ax11-pm2  34577  bj-snsetex  34702  wl-equsal1i  35250  mbfresfi  35405  riscer  35728  vvdifopab  35983  opabf  36082  cnvcosseq  36144  symrelcoss3  36167  cotrintab  40709  pm11.11  41473  fun2dmnopgexmpl  44230  ichv  44356  ichf  44357  ichid  44358  icht  44359  ichcircshi  44361  icheq  44369