Theorem exlimivv 1965

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 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  3495  cgsex4g  3496  opabss  5169  dtruALT2  5335  exneq  5411  copsexgw  5466  copsexgwOLD  5467  copsexg  5468  elopab  5505  0nelelxp  5690  elvvuni  5732  optocl  5749  optoclOLD  5750  relopabiALT  5804  relop  5830  elreldm  5919  xpnz  6151  xpdifid  6160  xpdifcnvepel  6161  dfco2a  6242  unielrel  6271  unixp0  6281  funsndifnop  7149  fmptsng  7167  oprabidw  7445  oprabid  7446  oprabv  7474  1stval2  8004  2ndval2  8005  1st2val  8015  2nd2val  8016  xp1st  8019  xp2nd  8020  frxp  8125  poxp  8127  soxp  8128  rntpos  8238  dftpos4  8244  tpostpos  8245  frrlem4  8289  tfrlem7  8373  ener  9008  domtr  9014  funen1cnv  9036  unen  9053  xpsnen  9060  undom  9064  sbthlem10  9095  mapen  9140  cnvfi  9171  entrfil  9180  domtrfil  9187  sbthfilem  9193  djuunxp  9927  fseqen  10031  dfac5lem4  10130  kmlem16  10169  axdc4lem  10458  hashfacen  14520  hashle2pr  14543  fundmge2nop0  14568  catcone0  17776  gictr  19404  dvdsrval  20503  rictr  20664  rngqiprngimfo  21505  thlle  21911  hmphtr  24010  fsumdvdsmul  27432  griedg0ssusgr  29726  rgrusgrprc  30050  loop1cycl  30624  numclwwlk1lem2fo  30839  frgrregord013  30876  friendship  30880  nvss  31075  spanuni  32026  5oalem7  32142  3oalem3  32146  opabssi  33087  gsummpt2co  33489  qqhval2  34493  bnj605  35417  bnj607  35426  fineqvac  35643  satfv1  35943  sat1el2xp  35959  fmla0xp  35963  satefvfmla0  35998  mppspstlem  36151  mppsval  36152  pprodss4v  36462  sscoid  36491  colinearex  36641  copsex2b  37893  pr2cv  44389  stoweidlem35  46864  funop1  48172  sprsymrelfvlem  48391  grictr  48840  uspgrsprf  49063  uspgrsprf1  49064  rrx2plordisom  49654  eloprab1st2nd  49797