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  2774  moeq  3646  csbie2  3867  mosneq  4733  eusv1  5257  moop2  5357  mosubop  5366  eqrelriv  5626  opabid2  5664  xpidtr  5949  fvmptopab  7188  funoprab  7253  mpofun  7255  fnoprab  7256  elovmpo  7370  wfrfun  7948  tfrlem7  8002  hartogs  8992  card2on  9002  epinid0  9048  cnvepnep  9055  tskwe  9363  ondomon  9974  fi1uzind  13851  brfi1indALT  13854  climeu  14904  letsr  17829  ulmdm  24988  wlkRes  27439  ajmoi  28641  helch  29026  hsn0elch  29031  chintcli  29114  adjmo  29615  nlelchi  29844  hmopidmchi  29934  bnj978  32331  bnj1052  32357  bnj1030  32369  funen1cnv  32467  satfv0  32718  satfv0fun  32731  fnsingle  33493  funimage  33502  funpartfun  33517  imagesset  33527  funtransport  33605  funray  33714  funline  33716  filnetlem3  33841  bj-cbvalimi  34093  bj-cbveximi  34094  ax11-pm  34270  ax11-pm2  34274  bj-snsetex  34399  wl-equsal1i  34948  mbfresfi  35103  riscer  35426  vvdifopab  35681  opabf  35780  cnvcosseq  35842  symrelcoss3  35865  cotrintab  40314  pm11.11  41078  fun2dmnopgexmpl  43840  ichv  43966  ichf  43967  ichid  43968  icht  43969  ichcircshi  43971  icheq  43979