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

Theorem gen2 1553
Description: Generalization applied twice. (Contributed by NM, 30-Apr-1998.)
Hypothesis
Ref Expression
gen2.1  |-  ph
Assertion
Ref Expression
gen2  |-  A. x A. y ph

Proof of Theorem gen2
StepHypRef Expression
1 gen2.1 . . 3  |-  ph
21ax-gen 1552 . 2  |-  A. y ph
32ax-gen 1552 1  |-  A. x A. y ph
Colors of variables: wff set class
Syntax hints:   A.wal 1546
This theorem is referenced by:  euequ1  2342  bm1.1  2389  vtocl3  2968  eueq  3066  csbie2  3256  moop2  4411  mosubop  4415  eusv1  4676  eqrelriv  4928  opabid2  4963  xpidtr  5215  funoprab  6129  mpt2fun  6131  fnoprab  6132  elovmpt2  6250  tfrlem7  6603  hartogs  7469  card2on  7478  tskwe  7793  ondomon  8394  brfi1uzind  11670  climeu  12304  letsr  14627  ulmdm  20262  ajmoi  22313  helch  22699  hsn0elch  22703  chintcli  22786  adjmo  23288  nlelchi  23517  hmopidmchi  23607  wfrlem11  25480  frrlem5c  25501  fnsingle  25672  funimage  25681  funpartfun  25696  funtransport  25869  funray  25978  funline  25980  mbfresfi  26152  filnetlem3  26299  riscer  26494  pm11.11  27438  bnj978  29026  bnj1052  29050  bnj1030  29062
This theorem was proved from axioms:  ax-gen 1552
  Copyright terms: Public domain W3C validator