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  5308  exneq  5384  copsexgw  5439  copsexg  5440  elopab  5476  0nelelxp  5660  elvvuni  5702  optocl  5719  optoclOLD  5720  relopabiALT  5773  relop  5800  elreldm  5885  xpnz  6118  xpdifid  6127  dfco2a  6205  unielrel  6233  unixp0  6242  funsndifnop  7099  fmptsng  7117  oprabidw  7392  oprabid  7393  oprabv  7421  1stval2  7953  2ndval2  7954  1st2val  7964  2nd2val  7965  xp1st  7968  xp2nd  7969  frxp  8070  poxp  8072  soxp  8073  rntpos  8183  dftpos4  8189  tpostpos  8190  frrlem4  8233  tfrlem7  8316  ener  8942  domtr  8948  unen  8986  xpsnen  8993  undom  8997  sbthlem10  9028  mapen  9073  cnvfi  9104  entrfil  9113  domtrfil  9120  sbthfilem  9126  djuunxp  9839  fseqen  9943  dfac5lem4  10042  dfac5lem4OLD  10044  kmlem16  10082  axdc4lem  10371  hashfacen  14410  hashle2pr  14433  fundmge2nop0  14458  catcone0  17647  gictr  19245  dvdsrval  20335  rngqiprngimfo  21294  thlle  21690  hmphtr  23761  fsumdvdsmul  27175  griedg0ssusgr  29351  rgrusgrprc  29676  numclwwlk1lem2fo  30446  frgrregord013  30483  friendship  30487  nvss  30682  spanuni  31633  5oalem7  31749  3oalem3  31753  opabssi  32704  gsummpt2co  33127  qqhval2  34145  bnj605  35068  bnj607  35077  funen1cnv  35250  fineqvac  35279  loop1cycl  35338  satfv1  35564  sat1el2xp  35580  fmla0xp  35584  satefvfmla0  35619  mppspstlem  35772  mppsval  35773  pprodss4v  36083  sscoid  36112  colinearex  36261  copsex2b  37473  rictr  42982  pr2cv  43996  stoweidlem35  46484  funop1  47746  sprsymrelfvlem  47965  grictr  48414  uspgrsprf  48637  uspgrsprf1  48638  rrx2plordisom  49214  eloprab1st2nd  49358