Theorem exlimivv 1932

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

Syntax hints:   → wi 4  ∃wex 1779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

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

This theorem is referenced by:  cgsex2g  3482  cgsex4g  3483  cgsex4gOLD  3484  opabss  5156  dtruALT2  5309  exneq  5379  copsexgw  5433  copsexg  5434  elopab  5470  0nelelxp  5654  elvvuni  5696  optocl  5713  optoclOLD  5714  relopabiALT  5766  relop  5793  elreldm  5877  xpnz  6108  xpdifid  6117  dfco2a  6195  unielrel  6222  unixp0  6231  funsndifnop  7085  fmptsng  7104  oprabidw  7380  oprabid  7381  oprabv  7409  1stval2  7941  2ndval2  7942  1st2val  7952  2nd2val  7953  xp1st  7956  xp2nd  7957  frxp  8059  poxp  8061  soxp  8062  rntpos  8172  dftpos4  8178  tpostpos  8179  frrlem4  8222  tfrlem7  8305  ener  8926  domtr  8932  unen  8971  xpsnen  8978  undom  8982  sbthlem10  9013  mapen  9058  cnvfi  9090  entrfil  9099  domtrfil  9106  sbthfilem  9112  djuunxp  9817  fseqen  9921  dfac5lem4  10020  dfac5lem4OLD  10022  kmlem16  10060  axdc4lem  10349  hashfacen  14361  hashle2pr  14384  fundmge2nop0  14409  catcone0  17593  gictr  19155  dvdsrval  20246  rngqiprngimfo  21208  thlle  21604  hmphtr  23668  fsumdvdsmul  27103  griedg0ssusgr  29210  rgrusgrprc  29535  numclwwlk1lem2fo  30302  frgrregord013  30339  friendship  30343  nvss  30537  spanuni  31488  5oalem7  31604  3oalem3  31608  opabssi  32558  gsummpt2co  33001  qqhval2  33949  bnj605  34874  bnj607  34883  funen1cnv  35055  fineqvac  35072  loop1cycl  35110  satfv1  35336  sat1el2xp  35352  fmla0xp  35356  satefvfmla0  35391  mppspstlem  35544  mppsval  35545  pprodss4v  35858  sscoid  35887  colinearex  36034  copsex2b  37114  rictr  42493  pr2cv  43521  stoweidlem35  46016  funop1  47267  sprsymrelfvlem  47474  grictr  47907  uspgrsprf  48130  uspgrsprf1  48131  rrx2plordisom  48708  eloprab1st2nd  48852