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

Theorem exlimivv 1900
Description: Inference form of Theorem 19.23 of [Margaris] p. 90, see 19.23 2118. (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 1898 . 2 (∃𝑦𝜑𝜓)
32exlimiv 1898 1 (∃𝑥𝑦𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1744
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879
This theorem depends on definitions:  df-bi 197  df-ex 1745
This theorem is referenced by:  cgsex2g  3270  cgsex4g  3271  opabss  4747  dtru  4887  copsexg  4985  elopab  5012  elopabr  5042  epelg  5059  0nelelxp  5179  elvvuni  5213  optocl  5229  relopabiALT  5279  relop  5305  elreldm  5382  xpnz  5588  xpdifid  5597  dfco2a  5673  unielrel  5698  unixp0  5707  funsndifnop  6456  fmptsng  6475  oprabid  6717  oprabv  6745  1stval2  7227  2ndval2  7228  1st2val  7238  2nd2val  7239  xp1st  7242  xp2nd  7243  frxp  7332  poxp  7334  soxp  7335  rntpos  7410  dftpos4  7416  tpostpos  7417  wfrlem4  7463  wfrfun  7470  tfrlem7  7524  ener  8044  domtr  8050  unen  8081  xpsnen  8085  sbthlem10  8120  mapen  8165  fseqen  8888  dfac5lem4  8987  kmlem16  9025  axdc4lem  9315  hashfacen  13276  hashle2pr  13297  fundmge2nop0  13312  gictr  17764  dvdsrval  18691  thlle  20089  hmphtr  21634  griedg0ssusgr  26202  rgrusgrprc  26541  numclwlk1lem2fo  27348  frgrregord013  27382  friendship  27386  nvss  27576  spanuni  28531  5oalem7  28647  3oalem3  28651  opabssi  29551  gsummpt2co  29908  qqhval2  30154  bnj605  31103  bnj607  31112  mppspstlem  31594  mppsval  31595  frrlem4  31908  frrlem5c  31911  pprodss4v  32116  sscoid  32145  colinearex  32292  bj-dtru  32922  stoweidlem35  40570  funop1  41625  sprsymrelfvlem  42065  uspgrsprf  42079  uspgrsprf1  42080
  Copyright terms: Public domain W3C validator