Theorem exlimivv 1933

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

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

This theorem is referenced by:  cgsex2g  3456  cgsex4g  3457  cgsex4gOLD  3458  opabss  5100  dtru  5243  copsexgw  5353  copsexg  5354  elopab  5388  elopabr  5421  0nelelxp  5563  elvvuni  5602  optocl  5619  relopabiALT  5670  relop  5696  elreldm  5781  xpnz  5993  xpdifid  6002  dfco2a  6081  unielrel  6108  unixp0  6117  funsndifnop  6910  fmptsng  6927  oprabidw  7187  oprabid  7188  oprabv  7214  1stval2  7716  2ndval2  7717  1st2val  7727  2nd2val  7728  xp1st  7731  xp2nd  7732  frxp  7831  poxp  7833  soxp  7834  rntpos  7921  dftpos4  7927  tpostpos  7928  wfrlem4  7974  wfrfun  7981  tfrlem7  8035  ener  8587  domtr  8593  unen  8629  xpsnen  8635  sbthlem10  8671  mapen  8716  djuunxp  9396  fseqen  9500  dfac5lem4  9599  kmlem16  9638  axdc4lem  9928  hashfacen  13875  hashfacenOLD  13876  hashle2pr  13900  fundmge2nop0  13915  gictr  18495  dvdsrval  19479  thlle  20475  hmphtr  22496  griedg0ssusgr  27167  rgrusgrprc  27491  numclwwlk1lem2fo  28255  frgrregord013  28292  friendship  28296  nvss  28488  spanuni  29439  5oalem7  29555  3oalem3  29559  opabssi  30488  gsummpt2co  30846  qqhval2  31463  bnj605  32419  bnj607  32428  funen1cnv  32592  loop1cycl  32627  satfv1  32853  sat1el2xp  32869  fmla0xp  32873  satefvfmla0  32908  mppspstlem  33061  mppsval  33062  frrlem4  33400  pprodss4v  33769  sscoid  33798  colinearex  33945  bj-dtru  34569  copsex2b  34869  sn-dtru  39739  pr2cv  40655  stoweidlem35  43078  funop1  44256  sprsymrelfvlem  44424  uspgrsprf  44790  uspgrsprf1  44791  rrx2plordisom  45551