Theorem exlimivv 1939

Description: Inference form of Theorem 19.23 of [Margaris] p. 90, see 19.23 2223. (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

Step	Hyp	Ref	Expression
1		exlimivv.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	exlimiv 1937	. 2 ⊢ (∃𝑦𝜑 → 𝜓)
3	2	exlimiv 1937	1 ⊢ (∃𝑥∃𝑦𝜑 → 𝜓)

Syntax hints:   → wi 4  ∃wex 1786

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem depends on definitions:  df-bi 208  df-ex 1787

This theorem is referenced by:  cgsex2g  3476  cgsex4g  3477  opabss  5136  dtruALT2  5299  exneq  5375  copsexgw  5430  copsexgwOLD  5431  copsexg  5432  elopab  5469  0nelelxp  5653  elvvuni  5695  optocl  5712  optoclOLD  5713  relopabiALT  5766  relop  5792  elreldm  5877  xpnz  6110  xpdifid  6119  dfco2a  6197  unielrel  6225  unixp0  6234  funsndifnop  7094  fmptsng  7112  oprabidw  7387  oprabid  7388  oprabv  7416  1stval2  7948  2ndval2  7949  1st2val  7959  2nd2val  7960  xp1st  7963  xp2nd  7964  frxp  8066  poxp  8068  soxp  8069  rntpos  8179  dftpos4  8185  tpostpos  8186  frrlem4  8229  tfrlem7  8312  ener  8938  domtr  8944  unen  8982  xpsnen  8989  undom  8993  sbthlem10  9024  mapen  9069  cnvfi  9100  entrfil  9109  domtrfil  9116  sbthfilem  9122  djuunxp  9836  fseqen  9940  dfac5lem4  10039  dfac5lem4OLD  10041  kmlem16  10079  axdc4lem  10368  hashfacen  14407  hashle2pr  14430  fundmge2nop0  14455  catcone0  17644  gictr  19242  dvdsrval  20332  rngqiprngimfo  21294  thlle  21672  hmphtr  23766  fsumdvdsmul  27176  griedg0ssusgr  29352  rgrusgrprc  29676  numclwwlk1lem2fo  30446  frgrregord013  30483  friendship  30487  nvss  30682  spanuni  31633  5oalem7  31749  3oalem3  31753  opabssi  32705  gsummpt2co  33129  qqhval2  34166  bnj605  35089  bnj607  35098  funen1cnv  35269  fineqvac  35297  loop1cycl  35365  satfv1  35591  sat1el2xp  35607  fmla0xp  35611  satefvfmla0  35646  mppspstlem  35799  mppsval  35800  pprodss4v  36110  sscoid  36139  colinearex  36288  copsex2b  37500  rictr  43006  pr2cv  43992  stoweidlem35  46478  funop1  47746  sprsymrelfvlem  47965  grictr  48414  uspgrsprf  48637  uspgrsprf1  48638  rrx2plordisom  49214  eloprab1st2nd  49358