Theorem exlimivv 1931

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

Syntax hints:   → wi 4  ∃wex 1778

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909

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

This theorem is referenced by:  cgsex2g  3510  cgsex4g  3511  cgsex4gOLD  3512  opabss  5187  dtruALT2  5350  exneq  5420  dtruOLD  5426  copsexgw  5475  copsexg  5476  elopab  5512  elopabrOLD  5548  0nelelxp  5700  elvvuni  5742  optocl  5760  relopabiALT  5813  relop  5841  elreldm  5926  xpnz  6159  xpdifid  6168  dfco2a  6246  unielrel  6274  unixp0  6283  funsndifnop  7151  fmptsng  7170  oprabidw  7444  oprabid  7445  oprabv  7475  1stval2  8013  2ndval2  8014  1st2val  8024  2nd2val  8025  xp1st  8028  xp2nd  8029  frxp  8133  poxp  8135  soxp  8136  rntpos  8246  dftpos4  8252  tpostpos  8253  frrlem4  8296  wfrlem4OLD  8334  wfrfunOLD  8341  tfrlem7  8405  ener  9023  domtr  9029  unen  9068  xpsnen  9077  undom  9081  sbthlem10  9114  mapen  9163  cnvfi  9198  entrfil  9207  domtrfil  9214  sbthfilem  9220  djuunxp  9943  fseqen  10049  dfac5lem4  10148  dfac5lem4OLD  10150  kmlem16  10188  axdc4lem  10477  hashfacen  14476  hashle2pr  14499  fundmge2nop0  14524  catcone0  17702  gictr  19264  dvdsrval  20330  rngqiprngimfo  21274  thlle  21671  thlleOLD  21672  hmphtr  23738  fsumdvdsmul  27175  griedg0ssusgr  29211  rgrusgrprc  29536  numclwwlk1lem2fo  30306  frgrregord013  30343  friendship  30347  nvss  30541  spanuni  31492  5oalem7  31608  3oalem3  31612  opabssi  32561  gsummpt2co  32995  qqhval2  33958  bnj605  34896  bnj607  34905  funen1cnv  35077  fineqvac  35086  loop1cycl  35117  satfv1  35343  sat1el2xp  35359  fmla0xp  35363  satefvfmla0  35398  mppspstlem  35551  mppsval  35552  pprodss4v  35860  sscoid  35889  colinearex  36036  copsex2b  37116  rictr  42509  pr2cv  43538  stoweidlem35  46022  funop1  47268  sprsymrelfvlem  47450  grictr  47865  uspgrsprf  48035  uspgrsprf1  48036  rrx2plordisom  48617  eloprab1st2nd  48751