Theorem exlimivv 1931

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 1929	. 2 ⊢ (∃𝑦𝜑 → 𝜓)
3	2	exlimiv 1929	1 ⊢ (∃𝑥∃𝑦𝜑 → 𝜓)

Syntax hints:   → wi 4  ∃wex 1777

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

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

This theorem is referenced by:  cgsex2g  3537  cgsex4g  3538  cgsex4gOLD  3539  opabss  5230  dtruALT2  5388  exneq  5455  dtruOLD  5461  copsexgw  5510  copsexg  5511  elopab  5546  elopabrOLD  5582  0nelelxp  5735  elvvuni  5776  optocl  5794  relopabiALT  5847  relop  5875  elreldm  5960  xpnz  6190  xpdifid  6199  dfco2a  6277  unielrel  6305  unixp0  6314  funsndifnop  7185  fmptsng  7202  oprabidw  7479  oprabid  7480  oprabv  7510  1stval2  8047  2ndval2  8048  1st2val  8058  2nd2val  8059  xp1st  8062  xp2nd  8063  frxp  8167  poxp  8169  soxp  8170  rntpos  8280  dftpos4  8286  tpostpos  8287  frrlem4  8330  wfrlem4OLD  8368  wfrfunOLD  8375  tfrlem7  8439  ener  9061  domtr  9067  unen  9112  xpsnen  9121  undom  9125  sbthlem10  9158  mapen  9207  cnvfi  9243  entrfil  9251  domtrfil  9258  sbthfilem  9264  djuunxp  9990  fseqen  10096  dfac5lem4  10195  dfac5lem4OLD  10197  kmlem16  10235  axdc4lem  10524  hashfacen  14503  hashle2pr  14526  fundmge2nop0  14551  catcone0  17745  gictr  19316  dvdsrval  20387  rngqiprngimfo  21334  thlle  21739  thlleOLD  21740  hmphtr  23812  fsumdvdsmul  27256  griedg0ssusgr  29300  rgrusgrprc  29625  numclwwlk1lem2fo  30390  frgrregord013  30427  friendship  30431  nvss  30625  spanuni  31576  5oalem7  31692  3oalem3  31696  opabssi  32635  gsummpt2co  33031  qqhval2  33928  bnj605  34883  bnj607  34892  funen1cnv  35064  fineqvac  35073  loop1cycl  35105  satfv1  35331  sat1el2xp  35347  fmla0xp  35351  satefvfmla0  35386  mppspstlem  35539  mppsval  35540  pprodss4v  35848  sscoid  35877  colinearex  36024  copsex2b  37106  rictr  42475  pr2cv  43510  stoweidlem35  45956  funop1  47198  sprsymrelfvlem  47364  grictr  47776  uspgrsprf  47869  uspgrsprf1  47870  rrx2plordisom  48457