Theorem exlimivv 1933

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

Syntax hints:   → wi 4  ∃wex 1780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-ex 1781

This theorem is referenced by:  cgsex2g  3482  cgsex4g  3483  cgsex4gOLD  3484  opabss  5153  dtruALT2  5306  exneq  5376  copsexgw  5428  copsexg  5429  elopab  5465  0nelelxp  5649  elvvuni  5691  optocl  5708  optoclOLD  5709  relopabiALT  5762  relop  5789  elreldm  5874  xpnz  6106  xpdifid  6115  dfco2a  6193  unielrel  6221  unixp0  6230  funsndifnop  7084  fmptsng  7102  oprabidw  7377  oprabid  7378  oprabv  7406  1stval2  7938  2ndval2  7939  1st2val  7949  2nd2val  7950  xp1st  7953  xp2nd  7954  frxp  8056  poxp  8058  soxp  8059  rntpos  8169  dftpos4  8175  tpostpos  8176  frrlem4  8219  tfrlem7  8302  ener  8923  domtr  8929  unen  8967  xpsnen  8974  undom  8978  sbthlem10  9009  mapen  9054  cnvfi  9085  entrfil  9094  domtrfil  9101  sbthfilem  9107  djuunxp  9814  fseqen  9918  dfac5lem4  10017  dfac5lem4OLD  10019  kmlem16  10057  axdc4lem  10346  hashfacen  14361  hashle2pr  14384  fundmge2nop0  14409  catcone0  17593  gictr  19188  dvdsrval  20279  rngqiprngimfo  21238  thlle  21634  hmphtr  23698  fsumdvdsmul  27132  griedg0ssusgr  29243  rgrusgrprc  29568  numclwwlk1lem2fo  30338  frgrregord013  30375  friendship  30379  nvss  30573  spanuni  31524  5oalem7  31640  3oalem3  31644  opabssi  32596  gsummpt2co  33028  qqhval2  33995  bnj605  34919  bnj607  34928  funen1cnv  35100  fineqvac  35139  loop1cycl  35181  satfv1  35407  sat1el2xp  35423  fmla0xp  35427  satefvfmla0  35462  mppspstlem  35615  mppsval  35616  pprodss4v  35926  sscoid  35955  colinearex  36102  copsex2b  37182  rictr  42561  pr2cv  43589  stoweidlem35  46081  funop1  47322  sprsymrelfvlem  47529  grictr  47962  uspgrsprf  48185  uspgrsprf1  48186  rrx2plordisom  48763  eloprab1st2nd  48907