Theorem exlimivv 1933

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

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

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

This theorem is referenced by:  cgsex2g  3518  cgsex4g  3519  cgsex4gOLD  3520  cgsex4gOLDOLD  3521  opabss  5211  dtruALT2  5367  exneq  5434  dtruOLD  5440  copsexgw  5489  copsexg  5490  elopab  5526  elopabrOLD  5562  0nelelxp  5710  elvvuni  5751  optocl  5769  relopabiALT  5822  relop  5849  elreldm  5933  xpnz  6157  xpdifid  6166  dfco2a  6244  unielrel  6272  unixp0  6281  funsndifnop  7150  fmptsng  7167  oprabidw  7442  oprabid  7443  oprabv  7471  1stval2  7994  2ndval2  7995  1st2val  8005  2nd2val  8006  xp1st  8009  xp2nd  8010  frxp  8114  poxp  8116  soxp  8117  rntpos  8226  dftpos4  8232  tpostpos  8233  frrlem4  8276  wfrlem4OLD  8314  wfrfunOLD  8321  tfrlem7  8385  ener  8999  domtr  9005  unen  9048  xpsnen  9057  undom  9061  sbthlem10  9094  mapen  9143  cnvfi  9182  entrfil  9190  domtrfil  9197  sbthfilem  9203  djuunxp  9918  fseqen  10024  dfac5lem4  10123  kmlem16  10162  axdc4lem  10452  hashfacen  14417  hashfacenOLD  14418  hashle2pr  14442  fundmge2nop0  14457  catcone0  17635  gictr  19190  dvdsrval  20252  rngqiprngimfo  21060  thlle  21470  thlleOLD  21471  hmphtr  23507  griedg0ssusgr  28789  rgrusgrprc  29113  numclwwlk1lem2fo  29878  frgrregord013  29915  friendship  29919  nvss  30113  spanuni  31064  5oalem7  31180  3oalem3  31184  opabssi  32109  gsummpt2co  32470  qqhval2  33260  bnj605  34216  bnj607  34225  funen1cnv  34389  fineqvac  34395  loop1cycl  34426  satfv1  34652  sat1el2xp  34668  fmla0xp  34672  satefvfmla0  34707  mppspstlem  34860  mppsval  34861  pprodss4v  35160  sscoid  35189  colinearex  35336  copsex2b  36324  rictr  41399  pr2cv  42601  stoweidlem35  45049  funop1  46289  sprsymrelfvlem  46456  uspgrsprf  46822  uspgrsprf1  46823  rrx2plordisom  47496