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

Theorem exlimivv 1847
Description: Inference form of Theorem 19.23 of [Margaris] p. 90, see 19.23 2067. (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 1845 . 2 (∃𝑦𝜑𝜓)
32exlimiv 1845 1 (∃𝑥𝑦𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1695
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827
This theorem depends on definitions:  df-bi 196  df-ex 1696
This theorem is referenced by:  cgsex2g  3212  cgsex4g  3213  opabss  4646  dtru  4783  copsexg  4882  elopab  4908  elopabr  4937  epelg  4950  0nelelxp  5069  elvvuni  5102  optocl  5118  relopabiALT  5168  relop  5194  elreldm  5271  xpnz  5472  xpdifid  5481  dfco2a  5552  unielrel  5577  unixp0  5586  funsndifnop  6321  fmptsng  6339  oprabid  6576  oprabv  6601  1stval2  7076  2ndval2  7077  1st2val  7085  2nd2val  7086  xp1st  7089  xp2nd  7090  frxp  7174  poxp  7176  soxp  7177  rntpos  7252  dftpos4  7258  tpostpos  7259  wfrlem4  7305  wfrfun  7312  tfrlem7  7366  ener  7888  enerOLD  7889  domtr  7895  unen  7925  xpsnen  7929  sbthlem10  7964  mapen  8009  fseqen  8733  dfac5lem4  8832  kmlem16  8870  axdc4lem  9160  hashfacen  13095  fundmge2nop0  13129  gictr  17540  dvdsrval  18468  thlle  19860  hmphtr  21396  usgrac  25880  edgss  25881  cusgrarn  25988  3v3e3cycl2  26192  3v3e3cycl  26193  numclwlk1lem2fo  26622  frgraregord013  26645  friendship  26649  nvss  26832  spanuni  27787  5oalem7  27903  3oalem3  27907  gsummpt2co  29111  qqhval2  29354  bnj605  30231  bnj607  30240  mppspstlem  30722  mppsval  30723  frrlem4  31027  frrlem5c  31030  pprodss4v  31161  sscoid  31190  colinearex  31337  bj-dtru  31985  stoweidlem35  38928  funop1  40327  griedg0ssusgr  40489  rgrusgrprc  40789  av-numclwlk1lem2fo  41525  av-frgraregord013  41549  av-friendship  41553
  Copyright terms: Public domain W3C validator