Theorem exlimivv 1965

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

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

This theorem is used by:  cgsex2g  3496  cgsex4g  3497  opabss  5169  dtruALT2  5332  exneq  5404  copsexgw  5460  copsexgwOLD  5461  copsexg  5462  cotsexgw  5463  elopab  5501  0nelelxp  5686  elvvuni  5728  optocl  5745  optoclOLD  5746  relopabiALT  5801  relop  5828  elreldm  5917  xpnz  6150  xpdifid  6159  xpdifcnvepel  6160  dfco2a  6247  unielrel  6276  unixp0  6286  funsndifnop  7155  fmptsng  7173  oprabidw  7451  oprabid  7452  oprabv  7480  1stval2  8018  2ndval2  8019  1st2val  8029  2nd2val  8030  xp1st  8033  xp2nd  8034  frxp  8138  poxp  8140  soxp  8141  rntpos  8256  dftpos4  8262  tpostpos  8263  frrlem4  8307  tfrlem7  8391  ener  9028  domtr  9034  funen1cnv  9056  unen  9073  xpsnen  9080  undom  9084  sbthlem10  9115  mapen  9160  cnvfi  9191  entrfil  9200  domtrfil  9207  sbthfilem  9213  djuunxp  10002  fseqen  10106  dfac5lem4  10205  kmlem16  10244  axdc4lem  10533  hashfacen  14599  hashle2pr  14622  fundmge2nop0  14647  catcone0  17861  gictr  19490  dvdsrval  20591  rictr  20752  rngqiprngimfo  21597  thlle  22003  hmphtr  24102  fsumdvdsmul  27522  griedg0ssusgr  29846  rgrusgrprc  30170  loop1cycl  30744  numclwwlk1lem2fo  30959  frgrregord013  30996  friendship  31000  nvss  31195  spanuni  32146  5oalem7  32262  3oalem3  32266  opabssi  33207  gsummpt2co  33609  qqhval2  34614  bnj605  35537  bnj607  35546  fineqvac  35784  satfv1  36128  sat1el2xp  36144  fmla0xp  36148  satefvfmla0  36183  mppspstlem  36336  mppsval  36337  pprodss4v  36646  sscoid  36675  colinearex  36825  copsex2b  38061  pr2cv  44548  stoweidlem35  47044  funop1  48352  sprsymrelfvlem  48571  grictr  49020  uspgrsprf  49243  uspgrsprf1  49244  rrx2plordisom  49834  eloprab1st2nd  49977