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

Theorem gen2 1871
 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 1870 . 2 𝑦𝜑
32ax-gen 1870 1 𝑥𝑦𝜑
 Colors of variables: wff setvar class Syntax hints:  ∀wal 1629 This theorem was proved from axioms:  ax-gen 1870 This theorem is referenced by:  bm1.1  2756  vtocl3  3413  eueq  3530  csbie2  3712  eusv1  4991  moop2  5093  mosubop  5104  eqrelriv  5353  opabid2  5390  xpidtr  5659  fvmptopab  6844  funoprab  6907  mpt2fun  6909  fnoprab  6910  elovmpt2  7026  wfrfun  7578  tfrlem7  7632  hartogs  8605  card2on  8615  epinid0  8661  cnvepnep  8667  tskwe  8976  ondomon  9587  fi1uzind  13481  brfi1indALT  13484  climeu  14494  letsr  17435  ulmdm  24367  wlkRes  26781  ajmoi  28054  helch  28440  hsn0elch  28445  chintcli  28530  adjmo  29031  nlelchi  29260  hmopidmchi  29350  bnj978  31357  bnj1052  31381  bnj1030  31393  frrlem5c  32123  fnsingle  32363  funimage  32372  funpartfun  32387  imagesset  32397  funtransport  32475  funray  32584  funline  32586  filnetlem3  32712  ax11-pm  33154  ax11-pm2  33158  bj-dfclel  33218  bj-dfcleq  33223  bj-snsetex  33282  wl-equsal1i  33664  mbfresfi  33788  riscer  34119  vvdifopab  34367  opabf  34472  cnvcosseq  34534  symrelcoss3  34557  cotrintab  38447  pm11.11  39099  fun2dmnopgexmpl  41826
 Copyright terms: Public domain W3C validator