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  3490  cgsex4g  3491  cgsex4gOLD  3492  opabss  5166  dtruALT2  5320  exneq  5390  dtruOLD  5396  copsexgw  5445  copsexg  5446  elopab  5482  0nelelxp  5666  elvvuni  5708  optocl  5725  relopabiALT  5777  relop  5804  elreldm  5888  xpnz  6120  xpdifid  6129  dfco2a  6207  unielrel  6235  unixp0  6244  funsndifnop  7105  fmptsng  7124  oprabidw  7400  oprabid  7401  oprabv  7429  1stval2  7964  2ndval2  7965  1st2val  7975  2nd2val  7976  xp1st  7979  xp2nd  7980  frxp  8082  poxp  8084  soxp  8085  rntpos  8195  dftpos4  8201  tpostpos  8202  frrlem4  8245  tfrlem7  8328  ener  8949  domtr  8955  unen  8994  xpsnen  9002  undom  9006  sbthlem10  9037  mapen  9082  cnvfi  9117  entrfil  9126  domtrfil  9133  sbthfilem  9139  djuunxp  9850  fseqen  9956  dfac5lem4  10055  dfac5lem4OLD  10057  kmlem16  10095  axdc4lem  10384  hashfacen  14395  hashle2pr  14418  fundmge2nop0  14443  catcone0  17624  gictr  19184  dvdsrval  20246  rngqiprngimfo  21187  thlle  21582  hmphtr  23646  fsumdvdsmul  27081  griedg0ssusgr  29168  rgrusgrprc  29493  numclwwlk1lem2fo  30260  frgrregord013  30297  friendship  30301  nvss  30495  spanuni  31446  5oalem7  31562  3oalem3  31566  opabssi  32514  gsummpt2co  32961  qqhval2  33945  bnj605  34870  bnj607  34879  funen1cnv  35051  fineqvac  35060  loop1cycl  35097  satfv1  35323  sat1el2xp  35339  fmla0xp  35343  satefvfmla0  35378  mppspstlem  35531  mppsval  35532  pprodss4v  35845  sscoid  35874  colinearex  36021  copsex2b  37101  rictr  42481  pr2cv  43510  stoweidlem35  46006  funop1  47257  sprsymrelfvlem  47464  grictr  47896  uspgrsprf  48107  uspgrsprf1  48108  rrx2plordisom  48685  eloprab1st2nd  48829