Theorem gen2 1723

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

Syntax hints:  ∀wal 1481

This theorem was proved from axioms:  ax-gen 1722

This theorem is referenced by:  bm1.1  2607  vtocl3  3262  eueq  3378  csbie2  3563  eusv1  4860  moop2  4966  mosubop  4973  eqrelriv  5213  opabid2  5251  xpidtr  5518  fvmptopab  6697  funoprab  6760  mpt2fun  6762  fnoprab  6763  elovmpt2  6879  wfrfun  7425  tfrlem7  7479  hartogs  8449  card2on  8459  tskwe  8776  ondomon  9385  fi1uzind  13279  brfi1indALT  13282  fi1uzindOLD  13285  brfi1indALTOLD  13288  climeu  14286  letsr  17227  ulmdm  24147  wlkRes  26546  ajmoi  27714  helch  28100  hsn0elch  28105  chintcli  28190  adjmo  28691  nlelchi  28920  hmopidmchi  29010  bnj978  31019  bnj1052  31043  bnj1030  31055  frrlem5c  31786  fnsingle  32026  funimage  32035  funpartfun  32050  imagesset  32060  funtransport  32138  funray  32247  funline  32249  filnetlem3  32375  ax11-pm  32819  ax11-pm2  32823  bj-dfclel  32889  bj-dfcleq  32894  bj-snsetex  32951  wl-equsal1i  33329  mbfresfi  33456  riscer  33787  vvdifopab  34024  cotrintab  37921  pm11.11  38573  fun2dmnopgexmpl  41303