Theorem gen2 1714

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

Syntax hints:  ∀wal 1473

This theorem was proved from axioms:  ax-gen 1713

This theorem is referenced by:  bm1.1  2595  vtocl3  3235  eueq  3345  csbie2  3529  eusv1  4786  moop2  4891  mosubop  4898  eqrelriv  5136  opabid2  5173  xpidtr  5437  fvmptopab1  6594  funoprab  6658  mpt2fun  6660  fnoprab  6661  elovmpt2  6777  wfrfun  7312  tfrlem7  7366  hartogs  8332  card2on  8342  tskwe  8659  ondomon  9264  fi1uzind  13134  brfi1indALT  13137  fi1uzindOLD  13140  brfi1indALTOLD  13143  climeu  14134  letsr  17050  ulmdm  23951  wlkres  26050  crcts  26150  cycls  26151  ajmoi  27098  helch  27484  hsn0elch  27489  chintcli  27574  adjmo  28075  nlelchi  28304  hmopidmchi  28394  bnj978  30273  bnj1052  30297  bnj1030  30309  frrlem5c  31030  fnsingle  31196  funimage  31205  funpartfun  31220  imagesset  31230  funtransport  31308  funray  31417  funline  31419  filnetlem3  31545  ax11-pm  32007  ax11-pm2  32011  bj-snsetex  32144  wl-equsal1i  32508  mbfresfi  32626  riscer  32957  cotrintab  36940  pm11.11  37595  fun2dmnopgexmpl  40329  wlkRes  40858