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  2326  bm1.1  2372  vtocl3  2951  eueq  3049  csbie2  3239  moop2  4392  mosubop  4396  eusv1  4657  eqrelriv  4909  opabid2  4944  xpidtr  5196  funoprab  6109  mpt2fun  6111  fnoprab  6112  elovmpt2  6230  tfrlem7  6580  hartogs  7446  card2on  7455  tskwe  7770  ondomon  8371  brfi1uzind  11642  climeu  12276  letsr  14599  ulmdm  20176  ajmoi  22208  helch  22594  hsn0elch  22598  chintcli  22681  adjmo  23183  nlelchi  23412  hmopidmchi  23502  wfrlem11  25290  frrlem5c  25311  fnsingle  25482  funimage  25491  funpartfun  25506  funtransport  25679  funray  25788  funline  25790  filnetlem3  26100  riscer  26295  pm11.11  27239  bnj978  28658  bnj1052  28682  bnj1030  28694
This theorem was proved from axioms:  ax-gen 1552
  Copyright terms: Public domain W3C validator