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  2739  moeq  3668  csbie2  3890  mosneq  4800  eusv1  5358  moop2  5479  mosubop  5488  eqrelriv  5771  opabid2  5813  xpidtr  6129  funoprab  7568  fnoprab  7571  elovmpo  7693  funmpt3  7714  mpt3fvd  7715  tfrlem7  8422  funen1cnv  9087  hartogs  9568  card2on  9578  epinid0  9629  cnvepnep  9639  ssttrcl  9746  tskwe  10061  ondomon  10677  fi1uzind  14682  brfi1indALT  14685  climeu  15754  letsr  18799  ulmdm  26753  ajmoi  31493  helch  31878  hsn0elch  31883  chintcli  31966  adjmo  32467  nlelchi  32696  hmopidmchi  32786  bnj978  35662  bnj1052  35688  bnj1030  35700  axsepg4  35924  satfv0  36303  satfv0fun  36316  fnsingle  36872  funimage  36881  funpartfun  36898  imagesset  36908  funtransport  36987  funray  37096  funline  37098  filnetlem3  37359  ttctr  37472  dfttc2g  37485  dfttc4lem2  37508  ax11-pm  37935  ax11-pm2  37939  bj-snsetex  38067  wl-equsal1i  38681  mbfresfi  38789  riscer  39125  vvdifopab  39400  opabf  39511  mopre  39606  cnvcosseq  39662  antisymressn  39669  trressn  39670  symrelcoss3  39690  cotrintab  44817  pm11.11  45561  fun2dmnopgexmpl  48569  ichv  48746  ichf  48747  ichid  48748  icht  48749  ichcircshi  48751  icheq  48759  pg4cyclnex  49440  mof0ALT  50166  f1omoOLD  50223