Theorem exlimivv 1934

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

Syntax hints:   → wi 4  ∃wex 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

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

This theorem is referenced by:  cgsex2g  3476  cgsex4g  3477  opabss  5150  dtruALT2  5313  exneq  5389  copsexgw  5444  copsexgwOLD  5445  copsexg  5446  elopab  5483  0nelelxp  5667  elvvuni  5709  optocl  5726  optoclOLD  5727  relopabiALT  5780  relop  5807  elreldm  5892  xpnz  6125  xpdifid  6134  dfco2a  6212  unielrel  6240  unixp0  6249  funsndifnop  7107  fmptsng  7125  oprabidw  7400  oprabid  7401  oprabv  7429  1stval2  7961  2ndval2  7962  1st2val  7972  2nd2val  7973  xp1st  7976  xp2nd  7977  frxp  8078  poxp  8080  soxp  8081  rntpos  8191  dftpos4  8197  tpostpos  8198  frrlem4  8241  tfrlem7  8324  ener  8950  domtr  8956  unen  8994  xpsnen  9001  undom  9005  sbthlem10  9036  mapen  9081  cnvfi  9112  entrfil  9121  domtrfil  9128  sbthfilem  9134  djuunxp  9847  fseqen  9951  dfac5lem4  10050  dfac5lem4OLD  10052  kmlem16  10090  axdc4lem  10379  hashfacen  14418  hashle2pr  14441  fundmge2nop0  14466  catcone0  17655  gictr  19253  dvdsrval  20343  rngqiprngimfo  21301  thlle  21679  hmphtr  23750  fsumdvdsmul  27160  griedg0ssusgr  29336  rgrusgrprc  29660  numclwwlk1lem2fo  30430  frgrregord013  30467  friendship  30471  nvss  30666  spanuni  31617  5oalem7  31733  3oalem3  31737  opabssi  32688  gsummpt2co  33111  qqhval2  34128  bnj605  35051  bnj607  35060  funen1cnv  35233  fineqvac  35262  loop1cycl  35321  satfv1  35547  sat1el2xp  35563  fmla0xp  35567  satefvfmla0  35602  mppspstlem  35755  mppsval  35756  pprodss4v  36066  sscoid  36095  colinearex  36244  copsex2b  37456  rictr  42967  pr2cv  43977  stoweidlem35  46465  funop1  47733  sprsymrelfvlem  47952  grictr  48401  uspgrsprf  48624  uspgrsprf1  48625  rrx2plordisom  49201  eloprab1st2nd  49345