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 1539

This theorem was proved from axioms:  ax-gen 1797

This theorem is referenced by:  axextmo  2706  moeq  3668  csbie2  3900  mosneq  4805  eusv1  5351  moop2  5464  mosubop  5473  eqrelriv  5750  opabid2  5789  xpidtr  6081  fvmptopabOLD  7417  funoprab  7483  mpofunOLD  7486  fnoprab  7487  elovmpo  7603  wfrfunOLD  8270  tfrlem7  8334  hartogs  9489  card2on  9499  epinid0  9545  cnvepnep  9553  ssttrcl  9660  tskwe  9895  ondomon  10508  fi1uzind  14408  brfi1indALT  14411  climeu  15449  letsr  18496  ulmdm  25789  wlkResOLD  28661  ajmoi  29863  helch  30248  hsn0elch  30253  chintcli  30336  adjmo  30837  nlelchi  31066  hmopidmchi  31156  bnj978  33650  bnj1052  33676  bnj1030  33688  funen1cnv  33781  satfv0  34039  satfv0fun  34052  fnsingle  34580  funimage  34589  funpartfun  34604  imagesset  34614  funtransport  34692  funray  34801  funline  34803  filnetlem3  34928  bj-cbvalimi  35187  bj-cbveximi  35188  ax11-pm  35373  ax11-pm2  35377  bj-snsetex  35507  wl-equsal1i  36075  mbfresfi  36197  riscer  36520  vvdifopab  36793  opabf  36902  cnvcosseq  36972  antisymressn  36979  trressn  36980  symrelcoss3  37000  cotrintab  42008  pm11.11  42776  fun2dmnopgexmpl  45636  ichv  45761  ichf  45762  ichid  45763  icht  45764  ichcircshi  45766  icheq  45774  mof0ALT  47026  f1omo  47047