Theorem gen2 1795

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

Syntax hints:  ∀wal 1537

This theorem was proved from axioms:  ax-gen 1794

This theorem is referenced by:  axextmo  2711  moeq  3712  csbie2  3937  mosneq  4841  eusv1  5390  moop2  5506  mosubop  5515  eqrelriv  5798  opabid2  5837  xpidtr  6141  fvmptopabOLD  7489  funoprab  7556  fnoprab  7559  elovmpo  7679  wfrfunOLD  8360  tfrlem7  8424  hartogs  9585  card2on  9595  epinid0  9641  cnvepnep  9649  ssttrcl  9756  tskwe  9991  ondomon  10604  fi1uzind  14547  brfi1indALT  14550  climeu  15592  letsr  18639  ulmdm  26437  wlkResOLD  29669  ajmoi  30878  helch  31263  hsn0elch  31268  chintcli  31351  adjmo  31852  nlelchi  32081  hmopidmchi  32171  bnj978  34964  bnj1052  34990  bnj1030  35002  funen1cnv  35103  satfv0  35364  satfv0fun  35377  fnsingle  35921  funimage  35930  funpartfun  35945  imagesset  35955  funtransport  36033  funray  36142  funline  36144  filnetlem3  36382  bj-cbvalimi  36649  bj-cbveximi  36650  ax11-pm  36834  ax11-pm2  36838  bj-snsetex  36965  wl-equsal1i  37546  mbfresfi  37674  riscer  37996  vvdifopab  38262  opabf  38370  cnvcosseq  38439  antisymressn  38446  trressn  38447  symrelcoss3  38467  cotrintab  43632  pm11.11  44398  fun2dmnopgexmpl  47301  ichv  47441  ichf  47442  ichid  47443  icht  47444  ichcircshi  47446  icheq  47454  mof0ALT  48754  f1omo  48798