MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  gen2 Structured version   Visualization version   GIF version

Theorem gen2 1722
Description: Generalization applied twice. (Contributed by NM, 30-Apr-1998.)
Hypothesis
Ref Expression
gen2.1 𝜑
Assertion
Ref Expression
gen2 𝑥𝑦𝜑

Proof of Theorem gen2
StepHypRef Expression
1 gen2.1 . . 3 𝜑
21ax-gen 1721 . 2 𝑦𝜑
32ax-gen 1721 1 𝑥𝑦𝜑
Colors of variables: wff setvar class
Syntax hints:  wal 1480
This theorem was proved from axioms:  ax-gen 1721
This theorem is referenced by:  bm1.1  2606  vtocl3  3260  eueq  3376  csbie2  3561  eusv1  4858  moop2  4964  mosubop  4971  eqrelriv  5211  opabid2  5249  xpidtr  5516  fvmptopab  6694  funoprab  6757  mpt2fun  6759  fnoprab  6760  elovmpt2  6876  wfrfun  7422  tfrlem7  7476  hartogs  8446  card2on  8456  tskwe  8773  ondomon  9382  fi1uzind  13274  brfi1indALT  13277  fi1uzindOLD  13280  brfi1indALTOLD  13283  climeu  14280  letsr  17221  ulmdm  24141  wlkRes  26540  ajmoi  27698  helch  28084  hsn0elch  28089  chintcli  28174  adjmo  28675  nlelchi  28904  hmopidmchi  28994  bnj978  31004  bnj1052  31028  bnj1030  31040  frrlem5c  31770  fnsingle  32010  funimage  32019  funpartfun  32034  imagesset  32044  funtransport  32122  funray  32231  funline  32233  filnetlem3  32359  ax11-pm  32803  ax11-pm2  32807  bj-dfclel  32873  bj-dfcleq  32878  bj-snsetex  32935  wl-equsal1i  33309  mbfresfi  33436  riscer  33767  cotrintab  37747  pm11.11  38399  fun2dmnopgexmpl  41072
  Copyright terms: Public domain W3C validator