Theorem exlimivv 1967

Description: Inference form of Theorem 19.23 of [Margaris] p. 90, see 19.23 2251. (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 1965	. 2 ⊢ (∃𝑦𝜑 → 𝜓)
3	2	exlimiv 1965	1 ⊢ (∃𝑥∃𝑦𝜑 → 𝜓)

This proof depends on syntax axioms:   → wi 4  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945

This proof depends on definitions:  df-bi 210  df-ex 1813

This theorem is used by:  cgsex2g  3499  cgsex4g  3500  opabss  5175  dtruALT2  5339  exneq  5411  copsexgw  5467  copsexgwOLD  5468  copsexg  5469  cotsexgw  5470  elopab  5508  0nelelxp  5693  elvvuni  5736  optocl  5753  optoclOLD  5754  relopabi  5809  relopabiALT  5811  relop  5838  elreldm  5929  xpnz  6168  xpdifid  6177  xpdifcnvepel  6178  dfco2a  6266  unielrel  6300  unixp0  6310  funsndifnop  7187  fmptsng  7204  oprabidw  7482  oprabid  7483  oprabv  7511  1stval2  8052  2ndval2  8053  1st2val  8063  2nd2val  8064  xp1st  8067  xp2nd  8068  frxp  8175  poxp  8177  soxp  8178  rntpos  8294  dftpos4  8300  tpostpos  8301  frrlem4  8345  tfrlem7  8429  ener  9066  domtr  9072  funen1cnv  9094  unen  9111  xpsnen  9118  undom  9122  sbthlem10  9153  mapen  9198  cnvfi  9229  entrfil  9238  domtrfil  9245  sbthfilem  9251  djuunxp  10039  fseqen  10145  dfac5lem4  10244  kmlem16  10283  axdc4lem  10572  hashfacen  14640  hashle2pr  14663  fundmge2nop0  14688  catcone0  17911  gictr  19541  dvdsrval  20642  rictr  20803  rngqiprngimfo  21648  thlle  22058  hmphtr  24157  fsumdvdsmul  27579  griedg0ssusgr  29903  rgrusgrprc  30227  loop1cycl  30801  numclwwlk1lem2fo  31016  frgrregord013  31053  friendship  31057  nvss  31252  spanuni  32203  5oalem7  32319  3oalem3  32323  opabssi  33305  gsummpt2co  33708  qqhval2  34725  bnj605  35648  bnj607  35657  fineqvac  35925  satfv1  36336  sat1el2xp  36352  fmla0xp  36356  satefvfmla0  36391  mppspstlem  36544  mppsval  36545  pprodss4v  36861  sscoid  36890  colinearex  37040  copsex2b  38332  cbvex2ivw  43529  pr2cv  44810  stoweidlem35  47318  funop1  48626  sprsymrelfvlem  48845  grictr  49294  uspgrsprf  49517  uspgrsprf1  49518  rrx2plordisom  50167  eloprab1st2nd  50310