Theorem exlimivv 1933

Description: Inference form of Theorem 19.23 of [Margaris] p. 90, see 19.23 2216. (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 1780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-ex 1781

This theorem is referenced by:  cgsex2g  3484  cgsex4g  3485  cgsex4gOLD  3486  opabss  5160  dtruALT2  5313  exneq  5383  copsexgw  5436  copsexg  5437  elopab  5473  0nelelxp  5657  elvvuni  5699  optocl  5716  optoclOLD  5717  relopabiALT  5770  relop  5797  elreldm  5882  xpnz  6115  xpdifid  6124  dfco2a  6202  unielrel  6230  unixp0  6239  funsndifnop  7094  fmptsng  7112  oprabidw  7387  oprabid  7388  oprabv  7416  1stval2  7948  2ndval2  7949  1st2val  7959  2nd2val  7960  xp1st  7963  xp2nd  7964  frxp  8066  poxp  8068  soxp  8069  rntpos  8179  dftpos4  8185  tpostpos  8186  frrlem4  8229  tfrlem7  8312  ener  8936  domtr  8942  unen  8980  xpsnen  8987  undom  8991  sbthlem10  9022  mapen  9067  cnvfi  9098  entrfil  9107  domtrfil  9114  sbthfilem  9120  djuunxp  9831  fseqen  9935  dfac5lem4  10034  dfac5lem4OLD  10036  kmlem16  10074  axdc4lem  10363  hashfacen  14375  hashle2pr  14398  fundmge2nop0  14423  catcone0  17608  gictr  19203  dvdsrval  20295  rngqiprngimfo  21254  thlle  21650  hmphtr  23725  fsumdvdsmul  27159  griedg0ssusgr  29287  rgrusgrprc  29612  numclwwlk1lem2fo  30382  frgrregord013  30419  friendship  30423  nvss  30617  spanuni  31568  5oalem7  31684  3oalem3  31688  opabssi  32640  gsummpt2co  33080  qqhval2  34088  bnj605  35012  bnj607  35021  funen1cnv  35193  fineqvac  35221  loop1cycl  35280  satfv1  35506  sat1el2xp  35522  fmla0xp  35526  satefvfmla0  35561  mppspstlem  35714  mppsval  35715  pprodss4v  36025  sscoid  36054  colinearex  36203  copsex2b  37284  rictr  42717  pr2cv  43731  stoweidlem35  46221  funop1  47471  sprsymrelfvlem  47678  grictr  48111  uspgrsprf  48334  uspgrsprf1  48335  rrx2plordisom  48911  eloprab1st2nd  49055