Theorem exlimivv 1936

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

Syntax hints:   → wi 4  ∃wex 1783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-ex 1784

This theorem is referenced by:  cgsex2g  3465  cgsex4g  3466  cgsex4gOLD  3467  opabss  5134  dtru  5288  copsexgw  5398  copsexg  5399  elopab  5433  elopabr  5466  0nelelxp  5615  elvvuni  5654  optocl  5671  relopabiALT  5722  relop  5748  elreldm  5833  xpnz  6051  xpdifid  6060  dfco2a  6139  unielrel  6166  unixp0  6175  funsndifnop  7005  fmptsng  7022  oprabidw  7286  oprabid  7287  oprabv  7313  1stval2  7821  2ndval2  7822  1st2val  7832  2nd2val  7833  xp1st  7836  xp2nd  7837  frxp  7938  poxp  7940  soxp  7941  rntpos  8026  dftpos4  8032  tpostpos  8033  frrlem4  8076  wfrlem4OLD  8114  wfrfunOLD  8121  tfrlem7  8185  ener  8742  domtr  8748  unen  8790  xpsnen  8796  sbthlem10  8832  mapen  8877  cnvfi  8924  entrfil  8931  domtrfi  8938  sbthfilem  8941  djuunxp  9610  fseqen  9714  dfac5lem4  9813  kmlem16  9852  axdc4lem  10142  hashfacen  14094  hashfacenOLD  14095  hashle2pr  14119  fundmge2nop0  14134  catcone0  17313  gictr  18806  dvdsrval  19802  thlle  20814  hmphtr  22842  griedg0ssusgr  27535  rgrusgrprc  27859  numclwwlk1lem2fo  28623  frgrregord013  28660  friendship  28664  nvss  28856  spanuni  29807  5oalem7  29923  3oalem3  29927  opabssi  30854  gsummpt2co  31210  qqhval2  31832  bnj605  32787  bnj607  32796  funen1cnv  32960  fineqvac  32966  loop1cycl  32999  satfv1  33225  sat1el2xp  33241  fmla0xp  33245  satefvfmla0  33280  mppspstlem  33433  mppsval  33434  pprodss4v  34113  sscoid  34142  colinearex  34289  bj-dtru  34926  copsex2b  35238  sn-dtru  40116  pr2cv  41044  stoweidlem35  43466  funop1  44662  sprsymrelfvlem  44830  uspgrsprf  45196  uspgrsprf1  45197  rrx2plordisom  45957