Theorem exlimivv 1959

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

Syntax hints:   → wi 4  ∃wex 1806

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937

This theorem depends on definitions:  df-bi 210  df-ex 1807

This theorem is referenced by:  cgsex2g  3508  cgsex4g  3509  opabss  5179  dtruALT2  5342  exneq  5418  copsexgw  5473  copsexgwOLD  5474  copsexg  5475  elopab  5512  0nelelxp  5697  elvvuni  5739  optocl  5756  optoclOLD  5757  relopabiALT  5811  relop  5837  elreldm  5926  xpnz  6157  xpdifid  6166  xpdifcnvepel  6167  dfco2a  6248  unielrel  6276  unixp0  6285  funsndifnop  7149  fmptsng  7167  oprabidw  7442  oprabid  7443  oprabv  7471  1stval2  8002  2ndval2  8003  1st2val  8013  2nd2val  8014  xp1st  8017  xp2nd  8018  frxp  8121  poxp  8123  soxp  8124  rntpos  8234  dftpos4  8240  tpostpos  8241  frrlem4  8285  tfrlem7  8369  ener  8997  domtr  9003  unen  9041  xpsnen  9048  undom  9052  sbthlem10  9083  mapen  9128  cnvfi  9159  entrfil  9168  domtrfil  9175  sbthfilem  9181  djuunxp  9906  fseqen  10010  dfac5lem4  10109  kmlem16  10148  axdc4lem  10438  hashfacen  14490  hashle2pr  14513  fundmge2nop0  14538  catcone0  17742  gictr  19345  dvdsrval  20442  rngqiprngimfo  21411  thlle  21815  hmphtr  23908  fsumdvdsmul  27324  griedg0ssusgr  29555  rgrusgrprc  29879  numclwwlk1lem2fo  30649  frgrregord013  30686  friendship  30690  nvss  30885  spanuni  31836  5oalem7  31952  3oalem3  31956  opabssi  32898  gsummpt2co  33308  qqhval2  34316  bnj605  35239  bnj607  35248  funen1cnv  35419  fineqvac  35451  loop1cycl  35527  satfv1  35753  sat1el2xp  35769  fmla0xp  35773  satefvfmla0  35808  mppspstlem  35961  mppsval  35962  pprodss4v  36272  sscoid  36301  colinearex  36450  copsex2b  37671  rictr  43179  pr2cv  44165  stoweidlem35  46640  funop1  47908  sprsymrelfvlem  48127  grictr  48576  uspgrsprf  48799  uspgrsprf1  48800  rrx2plordisom  49387  eloprab1st2nd  49530