Theorem gen2 1871

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

Syntax hints:  ∀wal 1629

This theorem was proved from axioms:  ax-gen 1870

This theorem is referenced by:  bm1.1  2756  vtocl3  3413  eueq  3530  csbie2  3712  eusv1  4991  moop2  5093  mosubop  5104  eqrelriv  5351  opabid2  5388  xpidtr  5657  fvmptopab  6842  funoprab  6905  mpt2fun  6907  fnoprab  6908  elovmpt2  7024  wfrfun  7576  tfrlem7  7630  hartogs  8603  card2on  8613  epinid0  8659  cnvepnep  8665  tskwe  8974  ondomon  9585  fi1uzind  13474  brfi1indALT  13477  climeu  14487  letsr  17428  ulmdm  24360  wlkRes  26774  ajmoi  28047  helch  28433  hsn0elch  28438  chintcli  28523  adjmo  29024  nlelchi  29253  hmopidmchi  29343  bnj978  31350  bnj1052  31374  bnj1030  31386  frrlem5c  32116  fnsingle  32356  funimage  32365  funpartfun  32380  imagesset  32390  funtransport  32468  funray  32577  funline  32579  filnetlem3  32705  ax11-pm  33147  ax11-pm2  33151  bj-dfclel  33211  bj-dfcleq  33216  bj-snsetex  33275  wl-equsal1i  33657  mbfresfi  33781  riscer  34112  vvdifopab  34360  opabf  34465  cnvcosseq  34527  symrelcoss3  34550  cotrintab  38440  pm11.11  39092  fun2dmnopgexmpl  41819