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 1540

This theorem was proved from axioms:  ax-gen 1797

This theorem is referenced by:  axextmo  2713  moeq  3654  csbie2  3877  mosneq  4786  eusv1  5328  moop2  5450  mosubop  5459  eqrelriv  5738  opabid2  5777  xpidtr  6079  funoprab  7482  fnoprab  7485  elovmpo  7605  tfrlem7  8315  hartogs  9452  card2on  9462  epinid0  9511  cnvepnep  9520  ssttrcl  9627  tskwe  9865  ondomon  10476  fi1uzind  14460  brfi1indALT  14463  climeu  15508  letsr  18550  ulmdm  26371  ajmoi  30944  helch  31329  hsn0elch  31334  chintcli  31417  adjmo  31918  nlelchi  32147  hmopidmchi  32237  bnj978  35107  bnj1052  35133  bnj1030  35145  funen1cnv  35247  satfv0  35556  satfv0fun  35569  fnsingle  36115  funimage  36124  funpartfun  36141  imagesset  36151  funtransport  36229  funray  36338  funline  36340  filnetlem3  36578  ttctr  36691  dfttc2g  36704  dfttc4lem2  36727  ax11-pm  37155  ax11-pm2  37159  bj-snsetex  37286  wl-equsal1i  37883  mbfresfi  38001  riscer  38323  vvdifopab  38600  opabf  38711  mopre  38806  cnvcosseq  38862  antisymressn  38869  trressn  38870  symrelcoss3  38890  cotrintab  44059  pm11.11  44819  fun2dmnopgexmpl  47744  ichv  47921  ichf  47922  ichid  47923  icht  47924  ichcircshi  47926  icheq  47934  pg4cyclnex  48615  mof0ALT  49327  f1omoOLD  49381