Theorem exlimivv 1962

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

Syntax hints:   → wi 4  ∃wex 1809

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940

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

This theorem is referenced by:  cgsex2g  3500  cgsex4g  3501  opabss  5175  dtruALT2  5341  exneq  5417  copsexgw  5472  copsexgwOLD  5473  copsexg  5474  elopab  5511  0nelelxp  5696  elvvuni  5738  optocl  5755  optoclOLD  5756  relopabiALT  5810  relop  5836  elreldm  5925  xpnz  6156  xpdifid  6165  xpdifcnvepel  6166  dfco2a  6247  unielrel  6275  unixp0  6284  funsndifnop  7148  fmptsng  7166  oprabidw  7441  oprabid  7442  oprabv  7470  1stval2  7999  2ndval2  8000  1st2val  8010  2nd2val  8011  xp1st  8014  xp2nd  8015  frxp  8118  poxp  8120  soxp  8121  rntpos  8231  dftpos4  8237  tpostpos  8238  frrlem4  8282  tfrlem7  8366  ener  8994  domtr  9000  unen  9038  xpsnen  9045  undom  9049  sbthlem10  9080  mapen  9125  cnvfi  9156  entrfil  9165  domtrfil  9172  sbthfilem  9178  djuunxp  9903  fseqen  10007  dfac5lem4  10106  kmlem16  10145  axdc4lem  10434  hashfacen  14487  hashle2pr  14510  fundmge2nop0  14535  catcone0  17738  gictr  19341  dvdsrval  20439  rictr  20600  rngqiprngimfo  21441  thlle  21847  hmphtr  23940  fsumdvdsmul  27359  griedg0ssusgr  29615  rgrusgrprc  29939  numclwwlk1lem2fo  30709  frgrregord013  30746  friendship  30750  nvss  30945  spanuni  31896  5oalem7  32012  3oalem3  32016  opabssi  32958  gsummpt2co  33368  qqhval2  34372  bnj605  35295  bnj607  35304  funen1cnv  35477  fineqvac  35529  loop1cycl  35629  satfv1  35855  sat1el2xp  35871  fmla0xp  35875  satefvfmla0  35910  mppspstlem  36063  mppsval  36064  pprodss4v  36374  sscoid  36403  colinearex  36552  copsex2b  37784  pr2cv  44274  stoweidlem35  46749  funop1  48020  sprsymrelfvlem  48239  grictr  48688  uspgrsprf  48911  uspgrsprf1  48912  rrx2plordisom  49503  eloprab1st2nd  49646