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  3667  csbie2  3890  mosneq  4800  eusv1  5338  moop2  5458  mosubop  5467  eqrelriv  5746  opabid2  5785  xpidtr  6087  funoprab  7490  fnoprab  7493  elovmpo  7613  tfrlem7  8324  hartogs  9461  card2on  9471  epinid0  9520  cnvepnep  9529  ssttrcl  9636  tskwe  9874  ondomon  10485  fi1uzind  14442  brfi1indALT  14445  climeu  15490  letsr  18528  ulmdm  26370  ajmoi  30945  helch  31330  hsn0elch  31335  chintcli  31418  adjmo  31919  nlelchi  32148  hmopidmchi  32238  bnj978  35124  bnj1052  35150  bnj1030  35162  funen1cnv  35263  satfv0  35571  satfv0fun  35584  fnsingle  36130  funimage  36139  funpartfun  36156  imagesset  36166  funtransport  36244  funray  36353  funline  36355  filnetlem3  36593  bj-cbvalimi  36888  bj-cbveximi  36889  ax11-pm  37077  ax11-pm2  37081  bj-snsetex  37208  wl-equsal1i  37796  mbfresfi  37914  riscer  38236  vvdifopab  38513  opabf  38624  mopre  38719  cnvcosseq  38775  antisymressn  38782  trressn  38783  symrelcoss3  38803  cotrintab  43967  pm11.11  44727  fun2dmnopgexmpl  47641  ichv  47806  ichf  47807  ichid  47808  icht  47809  ichcircshi  47811  icheq  47819  pg4cyclnex  48484  mof0ALT  49196  f1omoOLD  49250