Theorem exlimivv 1965

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

This proof depends on syntax axioms:   → wi 4  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-ex 1813

This theorem is used by:  cgsex2g  3502  cgsex4g  3503  opabss  5177  dtruALT2  5343  exneq  5419  copsexgw  5474  copsexgwOLD  5475  copsexg  5476  elopab  5513  0nelelxp  5698  elvvuni  5740  optocl  5757  optoclOLD  5758  relopabiALT  5812  relop  5838  elreldm  5927  xpnz  6158  xpdifid  6167  xpdifcnvepel  6168  dfco2a  6249  unielrel  6278  unixp0  6288  funsndifnop  7154  fmptsng  7172  oprabidw  7450  oprabid  7451  oprabv  7479  1stval2  8009  2ndval2  8010  1st2val  8020  2nd2val  8021  xp1st  8024  xp2nd  8025  frxp  8128  poxp  8130  soxp  8131  rntpos  8241  dftpos4  8247  tpostpos  8248  frrlem4  8292  tfrlem7  8376  ener  9004  domtr  9010  funen1cnv  9032  unen  9049  xpsnen  9056  undom  9060  sbthlem10  9091  mapen  9136  cnvfi  9167  entrfil  9176  domtrfil  9183  sbthfilem  9189  djuunxp  9923  fseqen  10027  dfac5lem4  10126  kmlem16  10165  axdc4lem  10454  hashfacen  14509  hashle2pr  14532  fundmge2nop0  14557  catcone0  17765  gictr  19390  dvdsrval  20489  rictr  20650  rngqiprngimfo  21491  thlle  21897  hmphtr  23991  fsumdvdsmul  27410  griedg0ssusgr  29673  rgrusgrprc  29997  loop1cycl  30571  numclwwlk1lem2fo  30780  frgrregord013  30817  friendship  30821  nvss  31016  spanuni  31967  5oalem7  32083  3oalem3  32087  opabssi  33029  gsummpt2co  33432  qqhval2  34436  bnj605  35360  bnj607  35369  fineqvac  35586  satfv1  35892  sat1el2xp  35908  fmla0xp  35912  satefvfmla0  35947  mppspstlem  36100  mppsval  36101  pprodss4v  36411  sscoid  36440  colinearex  36589  copsex2b  37841  pr2cv  44332  stoweidlem35  46807  funop1  48078  sprsymrelfvlem  48297  grictr  48746  uspgrsprf  48969  uspgrsprf1  48970  rrx2plordisom  49560  eloprab1st2nd  49703