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  3475  cgsex4g  3476  opabss  5149  dtruALT2  5312  exneq  5388  copsexgw  5443  copsexgwOLD  5444  copsexg  5445  elopab  5482  0nelelxp  5666  elvvuni  5708  optocl  5725  optoclOLD  5726  relopabiALT  5779  relop  5805  elreldm  5890  xpnz  6123  xpdifid  6132  dfco2a  6210  unielrel  6238  unixp0  6247  funsndifnop  7105  fmptsng  7123  oprabidw  7398  oprabid  7399  oprabv  7427  1stval2  7959  2ndval2  7960  1st2val  7970  2nd2val  7971  xp1st  7974  xp2nd  7975  frxp  8076  poxp  8078  soxp  8079  rntpos  8189  dftpos4  8195  tpostpos  8196  frrlem4  8239  tfrlem7  8322  ener  8948  domtr  8954  unen  8992  xpsnen  8999  undom  9003  sbthlem10  9034  mapen  9079  cnvfi  9110  entrfil  9119  domtrfil  9126  sbthfilem  9132  djuunxp  9845  fseqen  9949  dfac5lem4  10048  dfac5lem4OLD  10050  kmlem16  10088  axdc4lem  10377  hashfacen  14416  hashle2pr  14439  fundmge2nop0  14464  catcone0  17653  gictr  19251  dvdsrval  20341  rngqiprngimfo  21299  thlle  21677  hmphtr  23748  fsumdvdsmul  27158  griedg0ssusgr  29334  rgrusgrprc  29658  numclwwlk1lem2fo  30428  frgrregord013  30465  friendship  30469  nvss  30664  spanuni  31615  5oalem7  31731  3oalem3  31735  opabssi  32686  gsummpt2co  33109  qqhval2  34126  bnj605  35049  bnj607  35058  funen1cnv  35231  fineqvac  35260  loop1cycl  35319  satfv1  35545  sat1el2xp  35561  fmla0xp  35565  satefvfmla0  35600  mppspstlem  35753  mppsval  35754  pprodss4v  36064  sscoid  36093  colinearex  36242  copsex2b  37454  rictr  42965  pr2cv  43975  stoweidlem35  46463  funop1  47731  sprsymrelfvlem  47950  grictr  48399  uspgrsprf  48622  uspgrsprf1  48623  rrx2plordisom  49199  eloprab1st2nd  49343