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

Theorem exlimivv 1723
Description: Inference form of Theorem 19.23 of [Margaris] p. 90, see 19.23 1910. (Contributed by NM, 1-Aug-1995.)
Hypothesis
Ref Expression
exlimivv.1
Assertion
Ref Expression
exlimivv
Distinct variable groups:   ,   ,

Proof of Theorem exlimivv
StepHypRef Expression
1 exlimivv.1 . . 3
21exlimiv 1722 . 2
32exlimiv 1722 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  E.wex 1612
This theorem is referenced by:  cgsex2g  3143  cgsex4g  3144  opabss  4513  dtru  4643  copsexg  4737  copsexgOLD  4738  elopab  4760  epelg  4797  0nelelxp  5033  elvvuni  5065  optocl  5081  xpsspw  5121  relopabi  5133  relop  5158  elreldm  5232  xpnz  5431  xpdifid  5440  dfco2a  5512  unielrel  5537  unixp0  5546  fmptsng  6092  oprabid  6323  oprabv  6345  1stval2  6817  2ndval2  6818  1st2val  6826  2nd2val  6827  xp1st  6830  xp2nd  6831  frxp  6910  poxp  6912  soxp  6913  rntpos  6987  dftpos4  6993  tpostpos  6994  tfrlem7  7071  ener  7582  domtr  7588  unen  7618  xpsnen  7621  sbthlem10  7656  mapen  7701  fseqen  8429  dfac5lem4  8528  kmlem16  8566  axdc4lem  8856  hashfacen  12503  hash2prd  12518  gictr  16323  dvdsrval  17294  thlle  18728  hmphtr  20284  usgrac  24351  edgss  24352  cusgrarn  24459  3v3e3cycl2  24664  3v3e3cycl  24665  numclwlk1lem2fo  25095  frgraregord013  25118  friendship  25122  nvss  25486  spanuni  26462  5oalem7  26578  3oalem3  26582  gsummpt2co  27771  qqhval2  27963  mppspstlem  28931  mppsval  28932  wfrlem4  29346  wfrlem11  29353  frrlem4  29390  frrlem5c  29393  pprodss4v  29534  sscoid  29563  colinearex  29710  areacirc  30112  stoweidlem35  31817  bnj605  33965  bnj607  33974  bj-dtru  34383
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704
This theorem depends on definitions:  df-bi 185  df-ex 1613
  Copyright terms: Public domain W3C validator