Theorem exlimivv 1932

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

Syntax hints:   → wi 4  ∃wex 1779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

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

This theorem is referenced by:  cgsex2g  3511  cgsex4g  3512  cgsex4gOLD  3513  opabss  5188  dtruALT2  5345  exneq  5415  dtruOLD  5421  copsexgw  5470  copsexg  5471  elopab  5507  elopabrOLD  5543  0nelelxp  5694  elvvuni  5736  optocl  5754  relopabiALT  5807  relop  5835  elreldm  5920  xpnz  6153  xpdifid  6162  dfco2a  6240  unielrel  6268  unixp0  6277  funsndifnop  7146  fmptsng  7165  oprabidw  7441  oprabid  7442  oprabv  7472  1stval2  8010  2ndval2  8011  1st2val  8021  2nd2val  8022  xp1st  8025  xp2nd  8026  frxp  8130  poxp  8132  soxp  8133  rntpos  8243  dftpos4  8249  tpostpos  8250  frrlem4  8293  wfrlem4OLD  8331  wfrfunOLD  8338  tfrlem7  8402  ener  9020  domtr  9026  unen  9065  xpsnen  9074  undom  9078  sbthlem10  9111  mapen  9160  cnvfi  9195  entrfil  9204  domtrfil  9211  sbthfilem  9217  djuunxp  9940  fseqen  10046  dfac5lem4  10145  dfac5lem4OLD  10147  kmlem16  10185  axdc4lem  10474  hashfacen  14477  hashle2pr  14500  fundmge2nop0  14525  catcone0  17704  gictr  19264  dvdsrval  20326  rngqiprngimfo  21267  thlle  21662  hmphtr  23726  fsumdvdsmul  27162  griedg0ssusgr  29249  rgrusgrprc  29574  numclwwlk1lem2fo  30344  frgrregord013  30381  friendship  30385  nvss  30579  spanuni  31530  5oalem7  31646  3oalem3  31650  opabssi  32598  gsummpt2co  33047  qqhval2  34018  bnj605  34943  bnj607  34952  funen1cnv  35124  fineqvac  35133  loop1cycl  35164  satfv1  35390  sat1el2xp  35406  fmla0xp  35410  satefvfmla0  35445  mppspstlem  35598  mppsval  35599  pprodss4v  35907  sscoid  35936  colinearex  36083  copsex2b  37163  rictr  42518  pr2cv  43547  stoweidlem35  46044  funop1  47292  sprsymrelfvlem  47484  grictr  47916  uspgrsprf  48101  uspgrsprf1  48102  rrx2plordisom  48683  eloprab1st2nd  48823