Theorem gen2 1803

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

Syntax hints:  ∀wal 1545

This theorem was proved from axioms:  ax-gen 1802

This theorem is referenced by:  axextmo  2716  moeq  3655  csbie2  3877  mosneq  4780  eusv1  5327  moop2  5450  mosubop  5459  eqrelriv  5739  opabid2  5778  xpidtr  6079  funoprab  7485  fnoprab  7488  elovmpo  7608  tfrlem7  8319  hartogs  9456  card2on  9466  epinid0  9517  cnvepnep  9527  ssttrcl  9634  tskwe  9872  ondomon  10483  fi1uzind  14467  brfi1indALT  14470  climeu  15515  letsr  18557  ulmdm  26383  ajmoi  30954  helch  31339  hsn0elch  31344  chintcli  31427  adjmo  31928  nlelchi  32157  hmopidmchi  32247  bnj978  35138  bnj1052  35164  bnj1030  35176  funen1cnv  35276  axsepg4  35331  satfv0  35593  satfv0fun  35606  fnsingle  36152  funimage  36161  funpartfun  36178  imagesset  36188  funtransport  36266  funray  36375  funline  36377  filnetlem3  36615  ttctr  36728  dfttc2g  36741  dfttc4lem2  36764  ax11-pm  37192  ax11-pm2  37196  bj-snsetex  37323  wl-equsal1i  37922  mbfresfi  38040  riscer  38362  vvdifopab  38639  opabf  38750  mopre  38845  cnvcosseq  38901  antisymressn  38908  trressn  38909  symrelcoss3  38929  cotrintab  44065  pm11.11  44825  fun2dmnopgexmpl  47754  ichv  47931  ichf  47932  ichid  47933  icht  47934  ichcircshi  47936  icheq  47944  pg4cyclnex  48625  mof0ALT  49337  f1omoOLD  49391