Theorem exlimivv 1936

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

Syntax hints:   → wi 4  ∃wex 1782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914

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

This theorem is referenced by:  cgsex2g  3520  cgsex4g  3521  cgsex4gOLD  3522  cgsex4gOLDOLD  3523  opabss  5213  dtruALT2  5369  exneq  5436  dtruOLD  5442  copsexgw  5491  copsexg  5492  elopab  5528  elopabrOLD  5564  0nelelxp  5712  elvvuni  5753  optocl  5771  relopabiALT  5824  relop  5851  elreldm  5935  xpnz  6159  xpdifid  6168  dfco2a  6246  unielrel  6274  unixp0  6283  funsndifnop  7149  fmptsng  7166  oprabidw  7440  oprabid  7441  oprabv  7469  1stval2  7992  2ndval2  7993  1st2val  8003  2nd2val  8004  xp1st  8007  xp2nd  8008  frxp  8112  poxp  8114  soxp  8115  rntpos  8224  dftpos4  8230  tpostpos  8231  frrlem4  8274  wfrlem4OLD  8312  wfrfunOLD  8319  tfrlem7  8383  ener  8997  domtr  9003  unen  9046  xpsnen  9055  undom  9059  sbthlem10  9092  mapen  9141  cnvfi  9180  entrfil  9188  domtrfil  9195  sbthfilem  9201  djuunxp  9916  fseqen  10022  dfac5lem4  10121  kmlem16  10160  axdc4lem  10450  hashfacen  14413  hashfacenOLD  14414  hashle2pr  14438  fundmge2nop0  14453  catcone0  17631  gictr  19149  dvdsrval  20175  thlle  21251  thlleOLD  21252  hmphtr  23287  griedg0ssusgr  28522  rgrusgrprc  28846  numclwwlk1lem2fo  29611  frgrregord013  29648  friendship  29652  nvss  29846  spanuni  30797  5oalem7  30913  3oalem3  30917  opabssi  31842  gsummpt2co  32200  qqhval2  32962  bnj605  33918  bnj607  33927  funen1cnv  34091  fineqvac  34097  loop1cycl  34128  satfv1  34354  sat1el2xp  34370  fmla0xp  34374  satefvfmla0  34409  mppspstlem  34562  mppsval  34563  pprodss4v  34856  sscoid  34885  colinearex  35032  copsex2b  36021  rictr  41095  pr2cv  42299  stoweidlem35  44751  funop1  45991  sprsymrelfvlem  46158  uspgrsprf  46524  uspgrsprf1  46525  rngqiprngimfo  46786  rrx2plordisom  47409