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

Theorem gen2 1556
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 1555 . 2  |-  A. y ph
32ax-gen 1555 1  |-  A. x A. y ph
Colors of variables: wff set class
Syntax hints:   A.wal 1549
This theorem is referenced by:  euequ1  2368  bm1.1  2420  vtocl3  3000  eueq  3098  csbie2  3288  moop2  4443  mosubop  4447  eusv1  4709  eqrelriv  4961  opabid2  4996  xpidtr  5248  funoprab  6162  mpt2fun  6164  fnoprab  6165  elovmpt2  6283  tfrlem7  6636  hartogs  7505  card2on  7514  tskwe  7829  ondomon  8430  brfi1uzind  11707  climeu  12341  letsr  14664  ulmdm  20301  ajmoi  22352  helch  22738  hsn0elch  22742  chintcli  22825  adjmo  23327  nlelchi  23556  hmopidmchi  23646  wfrlem11  25540  frrlem5c  25580  fnsingle  25756  funimage  25765  funpartfun  25780  imagesset  25790  funtransport  25957  funray  26066  funline  26068  mbfresfi  26243  filnetlem3  26400  riscer  26595  pm11.11  27538  bnj978  29257  bnj1052  29281  bnj1030  29293
This theorem was proved from axioms:  ax-gen 1555
  Copyright terms: Public domain W3C validator