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  2738  moeq  3668  csbie2  3889  mosneq  4805  eusv1  5360  moop2  5483  mosubop  5492  eqrelriv  5773  opabid2  5813  xpidtr  6120  funoprab  7539  fnoprab  7542  elovmpo  7663  tfrlem7  8376  funen1cnv  9039  hartogs  9520  card2on  9530  epinid0  9581  cnvepnep  9591  ssttrcl  9698  tskwe  9959  ondomon  10575  fi1uzind  14576  brfi1indALT  14579  climeu  15646  letsr  18687  ulmdm  26636  ajmoi  31347  helch  31732  hsn0elch  31737  chintcli  31820  adjmo  32321  nlelchi  32550  hmopidmchi  32640  bnj978  35466  bnj1052  35492  bnj1030  35504  axsepg4  35677  satfv0  35945  satfv0fun  35958  fnsingle  36504  funimage  36513  funpartfun  36530  imagesset  36540  funtransport  36619  funray  36728  funline  36730  filnetlem3  37007  ttctr  37120  dfttc2g  37133  dfttc4lem2  37156  ax11-pm  37583  ax11-pm2  37587  bj-snsetex  37715  wl-equsal1i  38315  mbfresfi  38423  riscer  38746  vvdifopab  39021  opabf  39132  mopre  39227  cnvcosseq  39283  antisymressn  39290  trressn  39291  symrelcoss3  39311  cotrintab  44462  pm11.11  45206  fun2dmnopgexmpl  48180  ichv  48357  ichf  48358  ichid  48359  icht  48360  ichcircshi  48362  icheq  48370  pg4cyclnex  49051  mof0ALT  49776  f1omoOLD  49828