Theorem gen2 1819

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

Syntax hints:  ∀wal 1561

This theorem was proved from axioms:  ax-gen 1818

This theorem is referenced by:  axextmo  2741  moeq  3673  csbie2  3894  mosneq  4802  eusv1  5352  moop2  5475  mosubop  5484  eqrelriv  5765  opabid2  5805  xpidtr  6112  funoprab  7522  fnoprab  7525  elovmpo  7645  tfrlem7  8358  hartogs  9494  card2on  9504  epinid0  9555  cnvepnep  9565  ssttrcl  9672  tskwe  9924  ondomon  10535  fi1uzind  14532  brfi1indALT  14535  climeu  15594  letsr  18637  ulmdm  26510  ajmoi  31115  helch  31500  hsn0elch  31505  chintcli  31588  adjmo  32089  nlelchi  32318  hmopidmchi  32408  bnj978  35249  bnj1052  35275  bnj1030  35287  funen1cnv  35387  axsepg4  35446  satfv0  35716  satfv0fun  35729  fnsingle  36275  funimage  36284  funpartfun  36301  imagesset  36311  funtransport  36389  funray  36498  funline  36500  filnetlem3  36748  ttctr  36861  dfttc2g  36874  dfttc4lem2  36897  ax11-pm  37324  ax11-pm2  37328  bj-snsetex  37455  wl-equsal1i  38054  mbfresfi  38172  riscer  38494  vvdifopab  38771  opabf  38882  mopre  38977  cnvcosseq  39033  antisymressn  39040  trressn  39041  symrelcoss3  39061  cotrintab  44197  pm11.11  44943  fun2dmnopgexmpl  47877  ichv  48054  ichf  48055  ichid  48056  icht  48057  ichcircshi  48059  icheq  48067  pg4cyclnex  48748  mof0ALT  49470  f1omoOLD  49524