Theorem exlimivv 1933

Description: Inference form of Theorem 19.23 of [Margaris] p. 90, see 19.23 2218. (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  3486  cgsex4g  3487  cgsex4gOLD  3488  opabss  5162  dtruALT2  5315  exneq  5385  copsexgw  5438  copsexg  5439  elopab  5475  0nelelxp  5659  elvvuni  5701  optocl  5718  optoclOLD  5719  relopabiALT  5772  relop  5799  elreldm  5884  xpnz  6117  xpdifid  6126  dfco2a  6204  unielrel  6232  unixp0  6241  funsndifnop  7096  fmptsng  7114  oprabidw  7389  oprabid  7390  oprabv  7418  1stval2  7950  2ndval2  7951  1st2val  7961  2nd2val  7962  xp1st  7965  xp2nd  7966  frxp  8068  poxp  8070  soxp  8071  rntpos  8181  dftpos4  8187  tpostpos  8188  frrlem4  8231  tfrlem7  8314  ener  8938  domtr  8944  unen  8982  xpsnen  8989  undom  8993  sbthlem10  9024  mapen  9069  cnvfi  9100  entrfil  9109  domtrfil  9116  sbthfilem  9122  djuunxp  9833  fseqen  9937  dfac5lem4  10036  dfac5lem4OLD  10038  kmlem16  10076  axdc4lem  10365  hashfacen  14377  hashle2pr  14400  fundmge2nop0  14425  catcone0  17610  gictr  19205  dvdsrval  20297  rngqiprngimfo  21256  thlle  21652  hmphtr  23727  fsumdvdsmul  27161  griedg0ssusgr  29338  rgrusgrprc  29663  numclwwlk1lem2fo  30433  frgrregord013  30470  friendship  30474  nvss  30668  spanuni  31619  5oalem7  31735  3oalem3  31739  opabssi  32691  gsummpt2co  33131  qqhval2  34139  bnj605  35063  bnj607  35072  funen1cnv  35244  fineqvac  35272  loop1cycl  35331  satfv1  35557  sat1el2xp  35573  fmla0xp  35577  satefvfmla0  35612  mppspstlem  35765  mppsval  35766  pprodss4v  36076  sscoid  36105  colinearex  36254  copsex2b  37345  rictr  42775  pr2cv  43789  stoweidlem35  46279  funop1  47529  sprsymrelfvlem  47736  grictr  48169  uspgrsprf  48392  uspgrsprf1  48393  rrx2plordisom  48969  eloprab1st2nd  49113