Theorem gen2 1793

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

Syntax hints:  ∀wal 1531

This theorem was proved from axioms:  ax-gen 1792

This theorem is referenced by:  axextmo  2797  moeq  3698  csbie2  3922  mosneq  4767  eusv1  5284  moop2  5385  mosubop  5394  eqrelriv  5657  opabid2  5695  xpidtr  5977  fvmptopab  7203  funoprab  7268  mpofun  7270  fnoprab  7271  elovmpo  7384  wfrfun  7959  tfrlem7  8013  hartogs  9002  card2on  9012  epinid0  9058  cnvepnep  9065  tskwe  9373  ondomon  9979  fi1uzind  13849  brfi1indALT  13852  climeu  14906  letsr  17831  ulmdm  24975  wlkRes  27425  ajmoi  28629  helch  29014  hsn0elch  29019  chintcli  29102  adjmo  29603  nlelchi  29832  hmopidmchi  29922  bnj978  32216  bnj1052  32242  bnj1030  32254  funen1cnv  32352  satfv0  32600  satfv0fun  32613  fnsingle  33375  funimage  33384  funpartfun  33399  imagesset  33409  funtransport  33487  funray  33596  funline  33598  filnetlem3  33723  bj-cbvalimi  33975  bj-cbveximi  33976  ax11-pm  34150  ax11-pm2  34154  bj-snsetex  34270  wl-equsal1i  34777  mbfresfi  34932  riscer  35260  vvdifopab  35515  opabf  35614  cnvcosseq  35676  symrelcoss3  35699  cotrintab  39967  pm11.11  40699  fun2dmnopgexmpl  43476  ichv  43602  ichf  43603  ichid  43604  ichcircshi  43605  icheq  43613