Theorem gen2 1815

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

Syntax hints:  ∀wal 1557

This theorem was proved from axioms:  ax-gen 1814

This theorem is referenced by:  axextmo  2737  moeq  3668  csbie2  3889  mosneq  4797  eusv1  5345  moop2  5468  mosubop  5477  eqrelriv  5757  opabid2  5797  xpidtr  6104  funoprab  7512  fnoprab  7515  elovmpo  7635  tfrlem7  8347  hartogs  9485  card2on  9495  epinid0  9546  cnvepnep  9556  ssttrcl  9663  tskwe  9901  ondomon  10513  fi1uzind  14513  brfi1indALT  14516  climeu  15572  letsr  18615  ulmdm  26443  ajmoi  31017  helch  31402  hsn0elch  31407  chintcli  31490  adjmo  31991  nlelchi  32220  hmopidmchi  32310  bnj978  35204  bnj1052  35230  bnj1030  35242  funen1cnv  35342  axsepg4  35399  satfv0  35668  satfv0fun  35681  fnsingle  36227  funimage  36236  funpartfun  36253  imagesset  36263  funtransport  36341  funray  36450  funline  36452  filnetlem3  36700  ttctr  36813  dfttc2g  36826  dfttc4lem2  36849  ax11-pm  37277  ax11-pm2  37281  bj-snsetex  37408  wl-equsal1i  38007  mbfresfi  38125  riscer  38447  vvdifopab  38724  opabf  38835  mopre  38930  cnvcosseq  38986  antisymressn  38993  trressn  38994  symrelcoss3  39014  cotrintab  44150  pm11.11  44910  fun2dmnopgexmpl  47838  ichv  48015  ichf  48016  ichid  48017  icht  48018  ichcircshi  48020  icheq  48028  pg4cyclnex  48709  mof0ALT  49421  f1omoOLD  49475