Theorem exlimivv 1934

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

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

This theorem is referenced by:  cgsex2g  3488  cgsex4g  3489  cgsex4gOLD  3490  opabss  5164  dtruALT2  5317  exneq  5392  copsexgw  5446  copsexg  5447  elopab  5483  0nelelxp  5667  elvvuni  5709  optocl  5726  optoclOLD  5727  relopabiALT  5780  relop  5807  elreldm  5892  xpnz  6125  xpdifid  6134  dfco2a  6212  unielrel  6240  unixp0  6249  funsndifnop  7106  fmptsng  7124  oprabidw  7399  oprabid  7400  oprabv  7428  1stval2  7960  2ndval2  7961  1st2val  7971  2nd2val  7972  xp1st  7975  xp2nd  7976  frxp  8078  poxp  8080  soxp  8081  rntpos  8191  dftpos4  8197  tpostpos  8198  frrlem4  8241  tfrlem7  8324  ener  8950  domtr  8956  unen  8994  xpsnen  9001  undom  9005  sbthlem10  9036  mapen  9081  cnvfi  9112  entrfil  9121  domtrfil  9128  sbthfilem  9134  djuunxp  9845  fseqen  9949  dfac5lem4  10048  dfac5lem4OLD  10050  kmlem16  10088  axdc4lem  10377  hashfacen  14389  hashle2pr  14412  fundmge2nop0  14437  catcone0  17622  gictr  19217  dvdsrval  20309  rngqiprngimfo  21268  thlle  21664  hmphtr  23739  fsumdvdsmul  27173  griedg0ssusgr  29350  rgrusgrprc  29675  numclwwlk1lem2fo  30445  frgrregord013  30482  friendship  30486  nvss  30681  spanuni  31632  5oalem7  31748  3oalem3  31752  opabssi  32703  gsummpt2co  33142  qqhval2  34160  bnj605  35083  bnj607  35092  funen1cnv  35265  fineqvac  35294  loop1cycl  35353  satfv1  35579  sat1el2xp  35595  fmla0xp  35599  satefvfmla0  35634  mppspstlem  35787  mppsval  35788  pprodss4v  36098  sscoid  36127  colinearex  36276  copsex2b  37395  rictr  42890  pr2cv  43904  stoweidlem35  46393  funop1  47643  sprsymrelfvlem  47850  grictr  48283  uspgrsprf  48506  uspgrsprf1  48507  rrx2plordisom  49083  eloprab1st2nd  49227