Theorem gen2 1802

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

Syntax hints:  ∀wal 1539

This theorem was proved from axioms:  ax-gen 1801

This theorem is referenced by:  axextmo  2714  moeq  3645  csbie2  3878  mosneq  4778  eusv1  5317  moop2  5418  mosubop  5427  eqrelriv  5696  opabid2  5735  xpidtr  6024  fvmptopab  7321  funoprab  7387  mpofunOLD  7390  fnoprab  7391  elovmpo  7505  wfrfunOLD  8134  tfrlem7  8198  hartogs  9264  card2on  9274  epinid0  9320  cnvepnep  9327  ssttrcl  9434  tskwe  9692  ondomon  10303  fi1uzind  14192  brfi1indALT  14195  climeu  15245  letsr  18292  ulmdm  25533  wlkRes  27997  ajmoi  29199  helch  29584  hsn0elch  29589  chintcli  29672  adjmo  30173  nlelchi  30402  hmopidmchi  30492  bnj978  32908  bnj1052  32934  bnj1030  32946  funen1cnv  33039  satfv0  33299  satfv0fun  33312  fnsingle  34200  funimage  34209  funpartfun  34224  imagesset  34234  funtransport  34312  funray  34421  funline  34423  filnetlem3  34548  bj-cbvalimi  34807  bj-cbveximi  34808  ax11-pm  34994  ax11-pm2  34998  bj-snsetex  35132  wl-equsal1i  35681  mbfresfi  35802  riscer  36125  vvdifopab  36378  opabf  36477  cnvcosseq  36539  symrelcoss3  36562  cotrintab  41175  pm11.11  41945  fun2dmnopgexmpl  44727  ichv  44853  ichf  44854  ichid  44855  icht  44856  ichcircshi  44858  icheq  44866  mof0ALT  46119  f1omo  46140