Theorem exlimivv 1932

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

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

This theorem is referenced by:  cgsex2g  3493  cgsex4g  3494  cgsex4gOLD  3495  opabss  5171  dtruALT2  5325  exneq  5395  dtruOLD  5401  copsexgw  5450  copsexg  5451  elopab  5487  elopabrOLD  5523  0nelelxp  5673  elvvuni  5715  optocl  5733  relopabiALT  5786  relop  5814  elreldm  5899  xpnz  6132  xpdifid  6141  dfco2a  6219  unielrel  6247  unixp0  6256  funsndifnop  7123  fmptsng  7142  oprabidw  7418  oprabid  7419  oprabv  7449  1stval2  7985  2ndval2  7986  1st2val  7996  2nd2val  7997  xp1st  8000  xp2nd  8001  frxp  8105  poxp  8107  soxp  8108  rntpos  8218  dftpos4  8224  tpostpos  8225  frrlem4  8268  tfrlem7  8351  ener  8972  domtr  8978  unen  9017  xpsnen  9025  undom  9029  sbthlem10  9060  mapen  9105  cnvfi  9140  entrfil  9149  domtrfil  9156  sbthfilem  9162  djuunxp  9874  fseqen  9980  dfac5lem4  10079  dfac5lem4OLD  10081  kmlem16  10119  axdc4lem  10408  hashfacen  14419  hashle2pr  14442  fundmge2nop0  14467  catcone0  17648  gictr  19208  dvdsrval  20270  rngqiprngimfo  21211  thlle  21606  hmphtr  23670  fsumdvdsmul  27105  griedg0ssusgr  29192  rgrusgrprc  29517  numclwwlk1lem2fo  30287  frgrregord013  30324  friendship  30328  nvss  30522  spanuni  31473  5oalem7  31589  3oalem3  31593  opabssi  32541  gsummpt2co  32988  qqhval2  33972  bnj605  34897  bnj607  34906  funen1cnv  35078  fineqvac  35087  loop1cycl  35124  satfv1  35350  sat1el2xp  35366  fmla0xp  35370  satefvfmla0  35405  mppspstlem  35558  mppsval  35559  pprodss4v  35872  sscoid  35901  colinearex  36048  copsex2b  37128  rictr  42508  pr2cv  43537  stoweidlem35  46033  funop1  47284  sprsymrelfvlem  47491  grictr  47923  uspgrsprf  48134  uspgrsprf1  48135  rrx2plordisom  48712  eloprab1st2nd  48856