Theorem exlimivv 1964

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

This proof depends on syntax axioms:   → wi 4  ∃wex 1811

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942

This proof depends on definitions:  df-bi 210  df-ex 1812

This theorem is used by:  cgsex2g  3495  cgsex4g  3496  opabss  5168  dtruALT2  5332  exneq  5404  copsexgw  5460  copsexgwOLD  5461  copsexg  5462  cotsexgw  5463  elopab  5501  0nelelxp  5686  elvvuni  5729  optocl  5746  optoclOLD  5747  relopabiALT  5802  relop  5829  elreldm  5918  xpnz  6152  xpdifid  6161  xpdifcnvepel  6162  dfco2a  6250  unielrel  6279  unixp0  6289  funsndifnop  7160  fmptsng  7177  oprabidw  7455  oprabid  7456  oprabv  7484  1stval2  8022  2ndval2  8023  1st2val  8033  2nd2val  8034  xp1st  8037  xp2nd  8038  frxp  8145  poxp  8147  soxp  8148  rntpos  8264  dftpos4  8270  tpostpos  8271  frrlem4  8315  tfrlem7  8399  ener  9036  domtr  9042  funen1cnv  9064  unen  9081  xpsnen  9088  undom  9092  sbthlem10  9123  mapen  9168  cnvfi  9199  entrfil  9208  domtrfil  9215  sbthfilem  9221  djuunxp  10009  fseqen  10113  dfac5lem4  10212  kmlem16  10251  axdc4lem  10540  hashfacen  14606  hashle2pr  14629  fundmge2nop0  14654  catcone0  17870  gictr  19499  dvdsrval  20600  rictr  20761  rngqiprngimfo  21606  thlle  22012  hmphtr  24111  fsumdvdsmul  27531  griedg0ssusgr  29855  rgrusgrprc  30179  loop1cycl  30753  numclwwlk1lem2fo  30968  frgrregord013  31005  friendship  31009  nvss  31204  spanuni  32155  5oalem7  32271  3oalem3  32275  opabssi  33258  gsummpt2co  33659  qqhval2  34664  bnj605  35587  bnj607  35596  fineqvac  35852  satfv1  36246  sat1el2xp  36262  fmla0xp  36266  satefvfmla0  36301  mppspstlem  36454  mppsval  36455  pprodss4v  36770  sscoid  36799  colinearex  36949  copsex2b  38198  pr2cv  44686  stoweidlem35  47181  funop1  48489  sprsymrelfvlem  48708  grictr  49157  uspgrsprf  49380  uspgrsprf1  49381  rrx2plordisom  49972  eloprab1st2nd  50115