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

Theorem exlimivv 2023
Description: Inference form of Theorem 19.23 of [Margaris] p. 90, see 19.23 2247. (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 2021 . 2 (∃𝑦𝜑𝜓)
32exlimiv 2021 1 (∃𝑥𝑦𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1859
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001
This theorem depends on definitions:  df-bi 198  df-ex 1860
This theorem is referenced by:  cgsex2g  3433  cgsex4g  3434  opabss  4908  dtru  5040  copsexg  5145  elopab  5178  elopabr  5208  epelg  5225  0nelelxp  5345  elvvuni  5379  optocl  5397  relopabiALT  5448  relop  5474  elreldm  5551  xpnz  5764  xpdifid  5773  dfco2a  5849  unielrel  5874  unixp0  5883  funsndifnop  6640  fmptsng  6659  oprabid  6905  oprabv  6933  1stval2  7415  2ndval2  7416  1st2val  7426  2nd2val  7427  xp1st  7430  xp2nd  7431  frxp  7521  poxp  7523  soxp  7524  rntpos  7600  dftpos4  7606  tpostpos  7607  wfrlem4  7653  wfrlem4OLD  7654  wfrfun  7661  tfrlem7  7715  ener  8239  domtr  8245  unen  8279  xpsnen  8283  sbthlem10  8318  mapen  8363  djuunxp  9030  fseqen  9133  dfac5lem4  9232  kmlem16  9272  axdc4lem  9562  hashfacen  13455  hashle2pr  13476  fundmge2nop0  13491  gictr  17919  dvdsrval  18847  thlle  20251  hmphtr  21800  griedg0ssusgr  26373  rgrusgrprc  26713  numclwwlk1lem2fo  27537  frgrregord013  27583  friendship  27587  nvss  27776  spanuni  28731  5oalem7  28847  3oalem3  28851  opabssi  29750  gsummpt2co  30105  qqhval2  30351  bnj605  31300  bnj607  31309  mppspstlem  31791  mppsval  31792  frrlem4  32104  frrlem5c  32107  pprodss4v  32312  sscoid  32341  colinearex  32488  bj-dtru  33111  cnfinltrel  33557  stoweidlem35  40731  funop1  41873  sprsymrelfvlem  42308  uspgrsprf  42322  uspgrsprf1  42323
  Copyright terms: Public domain W3C validator