Theorem gen2 1826

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

Syntax hints:  ∀wal 1568

This theorem was proved from axioms:  ax-gen 1825

This theorem is referenced by:  axextmo  2739  moeq  3671  csbie2  3893  mosneq  4808  eusv1  5364  moop2  5487  mosubop  5496  eqrelriv  5777  opabid2  5817  xpidtr  6124  funoprab  7534  fnoprab  7537  elovmpo  7657  tfrlem7  8371  hartogs  9507  card2on  9517  epinid0  9568  cnvepnep  9578  ssttrcl  9685  tskwe  9937  ondomon  10548  fi1uzind  14546  brfi1indALT  14549  climeu  15608  letsr  18650  ulmdm  26537  ajmoi  31191  helch  31576  hsn0elch  31581  chintcli  31664  adjmo  32165  nlelchi  32394  hmopidmchi  32484  bnj978  35318  bnj1052  35344  bnj1030  35356  funen1cnv  35458  axsepg4  35537  satfv0  35831  satfv0fun  35844  fnsingle  36390  funimage  36399  funpartfun  36416  imagesset  36426  funtransport  36504  funray  36613  funline  36615  filnetlem3  36872  ttctr  36985  dfttc2g  36998  dfttc4lem2  37021  ax11-pm  37448  ax11-pm2  37452  bj-snsetex  37580  wl-equsal1i  38180  mbfresfi  38298  riscer  38620  vvdifopab  38895  opabf  39006  mopre  39101  cnvcosseq  39157  antisymressn  39164  trressn  39165  symrelcoss3  39185  cotrintab  44323  pm11.11  45067  fun2dmnopgexmpl  48004  ichv  48181  ichf  48182  ichid  48183  icht  48184  ichcircshi  48186  icheq  48194  pg4cyclnex  48875  mof0ALT  49601  f1omoOLD  49655