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

Theorem exlimivv 1936
Description: Inference form of Theorem 19.23 of [Margaris] p. 90, see 19.23 2205. (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 1934 . 2 (∃𝑦𝜑𝜓)
32exlimiv 1934 1 (∃𝑥𝑦𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914
This theorem depends on definitions:  df-bi 206  df-ex 1783
This theorem is referenced by:  cgsex2g  3492  cgsex4g  3493  cgsex4gOLD  3494  opabss  5174  dtruALT2  5330  exneq  5397  dtruOLD  5403  copsexgw  5452  copsexg  5453  elopab  5489  elopabrOLD  5525  0nelelxp  5673  elvvuni  5713  optocl  5731  relopabiALT  5784  relop  5811  elreldm  5895  xpnz  6116  xpdifid  6125  dfco2a  6203  unielrel  6231  unixp0  6240  funsndifnop  7102  fmptsng  7119  oprabidw  7393  oprabid  7394  oprabv  7422  1stval2  7943  2ndval2  7944  1st2val  7954  2nd2val  7955  xp1st  7958  xp2nd  7959  frxp  8063  poxp  8065  soxp  8066  rntpos  8175  dftpos4  8181  tpostpos  8182  frrlem4  8225  wfrlem4OLD  8263  wfrfunOLD  8270  tfrlem7  8334  ener  8948  domtr  8954  unen  8997  xpsnen  9006  undom  9010  sbthlem10  9043  mapen  9092  cnvfi  9131  entrfil  9139  domtrfil  9146  sbthfilem  9152  djuunxp  9864  fseqen  9970  dfac5lem4  10069  kmlem16  10108  axdc4lem  10398  hashfacen  14358  hashfacenOLD  14359  hashle2pr  14383  fundmge2nop0  14398  catcone0  17574  gictr  19072  dvdsrval  20081  thlle  21118  thlleOLD  21119  hmphtr  23150  griedg0ssusgr  28255  rgrusgrprc  28579  numclwwlk1lem2fo  29344  frgrregord013  29381  friendship  29385  nvss  29577  spanuni  30528  5oalem7  30644  3oalem3  30648  opabssi  31574  gsummpt2co  31932  qqhval2  32603  bnj605  33559  bnj607  33568  funen1cnv  33732  fineqvac  33738  loop1cycl  33771  satfv1  33997  sat1el2xp  34013  fmla0xp  34017  satefvfmla0  34052  mppspstlem  34205  mppsval  34206  pprodss4v  34498  sscoid  34527  colinearex  34674  copsex2b  35640  rictr  40731  pr2cv  41894  stoweidlem35  44350  funop1  45589  sprsymrelfvlem  45756  uspgrsprf  46122  uspgrsprf1  46123  rrx2plordisom  46883
  Copyright terms: Public domain W3C validator