Theorem exlimivv 1935

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

Syntax hints:   → wi 4  ∃wex 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913

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

This theorem is referenced by:  cgsex2g  3519  cgsex4g  3520  cgsex4gOLD  3521  cgsex4gOLDOLD  3522  opabss  5211  dtruALT2  5367  exneq  5434  dtruOLD  5440  copsexgw  5489  copsexg  5490  elopab  5526  elopabrOLD  5562  0nelelxp  5710  elvvuni  5750  optocl  5768  relopabiALT  5821  relop  5848  elreldm  5932  xpnz  6155  xpdifid  6164  dfco2a  6242  unielrel  6270  unixp0  6279  funsndifnop  7145  fmptsng  7162  oprabidw  7436  oprabid  7437  oprabv  7465  1stval2  7988  2ndval2  7989  1st2val  7999  2nd2val  8000  xp1st  8003  xp2nd  8004  frxp  8108  poxp  8110  soxp  8111  rntpos  8220  dftpos4  8226  tpostpos  8227  frrlem4  8270  wfrlem4OLD  8308  wfrfunOLD  8315  tfrlem7  8379  ener  8993  domtr  8999  unen  9042  xpsnen  9051  undom  9055  sbthlem10  9088  mapen  9137  cnvfi  9176  entrfil  9184  domtrfil  9191  sbthfilem  9197  djuunxp  9912  fseqen  10018  dfac5lem4  10117  kmlem16  10156  axdc4lem  10446  hashfacen  14409  hashfacenOLD  14410  hashle2pr  14434  fundmge2nop0  14449  catcone0  17627  gictr  19143  dvdsrval  20167  thlle  21242  thlleOLD  21243  hmphtr  23278  griedg0ssusgr  28511  rgrusgrprc  28835  numclwwlk1lem2fo  29600  frgrregord013  29637  friendship  29641  nvss  29833  spanuni  30784  5oalem7  30900  3oalem3  30904  opabssi  31829  gsummpt2co  32187  qqhval2  32950  bnj605  33906  bnj607  33915  funen1cnv  34079  fineqvac  34085  loop1cycl  34116  satfv1  34342  sat1el2xp  34358  fmla0xp  34362  satefvfmla0  34397  mppspstlem  34550  mppsval  34551  pprodss4v  34844  sscoid  34873  colinearex  35020  copsex2b  36009  rictr  41092  pr2cv  42284  stoweidlem35  44737  funop1  45977  sprsymrelfvlem  46144  uspgrsprf  46510  uspgrsprf1  46511  rngqiprngimfo  46766  rrx2plordisom  47362