Theorem exlimivv 1952

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

Syntax hints:   → wi 4  ∃wex 1799

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930

This theorem depends on definitions:  df-bi 209  df-ex 1800

This theorem is referenced by:  cgsex2g  3499  cgsex4g  3500  opabss  5164  dtruALT2  5327  exneq  5403  copsexgw  5458  copsexgwOLD  5459  copsexg  5460  elopab  5497  0nelelxp  5682  elvvuni  5724  optocl  5741  optoclOLD  5742  relopabiALT  5796  relop  5822  elreldm  5911  xpnz  6144  xpdifid  6153  xpdifcnvepel  6154  dfco2a  6233  unielrel  6261  unixp0  6270  funsndifnop  7134  fmptsng  7152  oprabidw  7427  oprabid  7428  oprabv  7456  1stval2  7987  2ndval2  7988  1st2val  7998  2nd2val  7999  xp1st  8002  xp2nd  8003  frxp  8106  poxp  8108  soxp  8109  rntpos  8219  dftpos4  8225  tpostpos  8226  frrlem4  8270  tfrlem7  8354  ener  8982  domtr  8988  unen  9026  xpsnen  9033  undom  9037  sbthlem10  9068  mapen  9113  cnvfi  9144  entrfil  9153  domtrfil  9160  sbthfilem  9166  djuunxp  9879  fseqen  9983  dfac5lem4  10082  dfac5lem4OLD  10084  kmlem16  10122  axdc4lem  10412  hashfacen  14467  hashle2pr  14490  fundmge2nop0  14515  catcone0  17719  gictr  19316  dvdsrval  20410  rngqiprngimfo  21371  thlle  21749  hmphtr  23843  fsumdvdsmul  27259  griedg0ssusgr  29466  rgrusgrprc  29790  numclwwlk1lem2fo  30560  frgrregord013  30597  friendship  30601  nvss  30796  spanuni  31747  5oalem7  31863  3oalem3  31867  opabssi  32815  gsummpt2co  33228  qqhval2  34279  bnj605  35202  bnj607  35211  funen1cnv  35382  fineqvac  35412  loop1cycl  35487  satfv1  35713  sat1el2xp  35729  fmla0xp  35733  satefvfmla0  35768  mppspstlem  35921  mppsval  35922  pprodss4v  36232  sscoid  36261  colinearex  36410  copsex2b  37632  rictr  43138  pr2cv  44124  stoweidlem35  46609  funop1  47877  sprsymrelfvlem  48096  grictr  48545  uspgrsprf  48768  uspgrsprf1  48769  rrx2plordisom  49345  eloprab1st2nd  49489