Theorem gen2 1829

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

This proof depends on syntax axioms:  ∀wal 1568

This proof depends on axioms:  ax-gen 1828

This theorem is used by:  axextmo  2737  moeq  3665  csbie2  3886  mosneq  4802  eusv1  5353  moop2  5474  mosubop  5483  eqrelriv  5765  opabid2  5806  xpidtr  6114  funoprab  7534  fnoprab  7537  elovmpo  7658  funmpt3  7679  tfrlem7  8375  funen1cnv  9040  hartogs  9522  card2on  9532  epinid0  9583  cnvepnep  9593  ssttrcl  9700  tskwe  10012  ondomon  10628  fi1uzind  14632  brfi1indALT  14635  climeu  15702  letsr  18747  ulmdm  26702  ajmoi  31442  helch  31827  hsn0elch  31832  chintcli  31915  adjmo  32416  nlelchi  32645  hmopidmchi  32735  bnj978  35562  bnj1052  35588  bnj1030  35600  axsepg4  35784  satfv0  36092  satfv0fun  36105  fnsingle  36651  funimage  36660  funpartfun  36677  imagesset  36687  funtransport  36766  funray  36875  funline  36877  filnetlem3  37138  ttctr  37251  dfttc2g  37264  dfttc4lem2  37287  ax11-pm  37714  ax11-pm2  37718  bj-snsetex  37846  wl-equsal1i  38444  mbfresfi  38552  riscer  38890  vvdifopab  39165  opabf  39276  mopre  39371  cnvcosseq  39427  antisymressn  39434  trressn  39435  symrelcoss3  39455  cotrintab  44573  pm11.11  45317  fun2dmnopgexmpl  48298  ichv  48475  ichf  48476  ichid  48477  icht  48478  ichcircshi  48480  icheq  48488  pg4cyclnex  49169  mof0ALT  49894  f1omoOLD  49946