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

Theorem exlimivv 1858
Description: Inference form of Theorem 19.23 of [Margaris] p. 90, see 19.23 2078. (Contributed by NM, 1-Aug-1995.)
Hypothesis
Ref Expression
exlimivv.1 (𝜑𝜓)
Assertion
Ref Expression
exlimivv (∃𝑥𝑦𝜑𝜓)
Distinct variable groups:   𝜓,𝑥   𝜓,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)

Proof of Theorem exlimivv
StepHypRef Expression
1 exlimivv.1 . . 3 (𝜑𝜓)
21exlimiv 1856 . 2 (∃𝑦𝜑𝜓)
32exlimiv 1856 1 (∃𝑥𝑦𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1702
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837
This theorem depends on definitions:  df-bi 197  df-ex 1703
This theorem is referenced by:  cgsex2g  3234  cgsex4g  3235  opabss  4705  dtru  4848  copsexg  4946  elopab  4973  elopabr  5003  epelg  5020  0nelelxp  5135  elvvuni  5169  optocl  5185  relopabiALT  5235  relop  5261  elreldm  5339  xpnz  5541  xpdifid  5550  dfco2a  5623  unielrel  5648  unixp0  5657  funsndifnop  6401  fmptsng  6419  oprabid  6662  oprabv  6688  1stval2  7170  2ndval2  7171  1st2val  7179  2nd2val  7180  xp1st  7183  xp2nd  7184  frxp  7272  poxp  7274  soxp  7275  rntpos  7350  dftpos4  7356  tpostpos  7357  wfrlem4  7403  wfrfun  7410  tfrlem7  7464  ener  7987  enerOLD  7988  domtr  7994  unen  8025  xpsnen  8029  sbthlem10  8064  mapen  8109  fseqen  8835  dfac5lem4  8934  kmlem16  8972  axdc4lem  9262  hashfacen  13221  hashle2pr  13242  fundmge2nop0  13257  gictr  17698  dvdsrval  18626  thlle  20022  hmphtr  21567  griedg0ssusgr  26138  rgrusgrprc  26466  numclwlk1lem2fo  27199  frgrregord013  27223  friendship  27227  nvss  27418  spanuni  28373  5oalem7  28489  3oalem3  28493  gsummpt2co  29754  qqhval2  30000  bnj605  30951  bnj607  30960  mppspstlem  31442  mppsval  31443  frrlem4  31757  frrlem5c  31760  pprodss4v  31966  sscoid  31995  colinearex  32142  bj-dtru  32772  stoweidlem35  40015  funop1  41065  sprsymrelfvlem  41505  uspgrsprf  41519  uspgrsprf1  41520
  Copyright terms: Public domain W3C validator