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  2712  moeq  3653  csbie2  3876  mosneq  4785  eusv1  5333  moop2  5456  mosubop  5465  eqrelriv  5745  opabid2  5784  xpidtr  6085  funoprab  7489  fnoprab  7492  elovmpo  7612  tfrlem7  8322  hartogs  9459  card2on  9469  epinid0  9519  cnvepnep  9529  ssttrcl  9636  tskwe  9874  ondomon  10485  fi1uzind  14469  brfi1indALT  14472  climeu  15517  letsr  18559  ulmdm  26358  ajmoi  30929  helch  31314  hsn0elch  31319  chintcli  31402  adjmo  31903  nlelchi  32132  hmopidmchi  32222  bnj978  35091  bnj1052  35117  bnj1030  35129  funen1cnv  35231  satfv0  35540  satfv0fun  35553  fnsingle  36099  funimage  36108  funpartfun  36125  imagesset  36135  funtransport  36213  funray  36322  funline  36324  filnetlem3  36562  ttctr  36675  dfttc2g  36688  dfttc4lem2  36711  ax11-pm  37139  ax11-pm2  37143  bj-snsetex  37270  wl-equsal1i  37869  mbfresfi  37987  riscer  38309  vvdifopab  38586  opabf  38697  mopre  38792  cnvcosseq  38848  antisymressn  38855  trressn  38856  symrelcoss3  38876  cotrintab  44041  pm11.11  44801  fun2dmnopgexmpl  47732  ichv  47909  ichf  47910  ichid  47911  icht  47912  ichcircshi  47914  icheq  47922  pg4cyclnex  48603  mof0ALT  49315  f1omoOLD  49369