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  2742  moeq  3673  csbie2  3895  mosneq  4812  eusv1  5367  moop2  5490  mosubop  5499  eqrelriv  5780  opabid2  5820  xpidtr  6127  funoprab  7545  fnoprab  7548  elovmpo  7668  tfrlem7  8379  funen1cnv  9035  hartogs  9516  card2on  9526  epinid0  9577  cnvepnep  9587  ssttrcl  9694  tskwe  9955  ondomon  10565  fi1uzind  14564  brfi1indALT  14567  climeu  15632  letsr  18674  ulmdm  26593  ajmoi  31247  helch  31632  hsn0elch  31637  chintcli  31720  adjmo  32221  nlelchi  32450  hmopidmchi  32540  bnj978  35369  bnj1052  35395  bnj1030  35407  axsepg4  35580  satfv0  35871  satfv0fun  35884  fnsingle  36430  funimage  36439  funpartfun  36456  imagesset  36466  funtransport  36544  funray  36653  funline  36655  filnetlem3  36932  ttctr  37045  dfttc2g  37058  dfttc4lem2  37081  ax11-pm  37508  ax11-pm2  37512  bj-snsetex  37640  wl-equsal1i  38240  mbfresfi  38358  riscer  38680  vvdifopab  38955  opabf  39066  mopre  39161  cnvcosseq  39217  antisymressn  39224  trressn  39225  symrelcoss3  39245  cotrintab  44381  pm11.11  45125  fun2dmnopgexmpl  48062  ichv  48239  ichf  48240  ichid  48241  icht  48242  ichcircshi  48244  icheq  48252  pg4cyclnex  48933  mof0ALT  49659  f1omoOLD  49713