Theorem exlimivv 1930

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

Syntax hints:   → wi 4  ∃wex 1776

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908

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

This theorem is referenced by:  cgsex2g  3525  cgsex4g  3526  cgsex4gOLD  3527  opabss  5212  dtruALT2  5376  exneq  5446  dtruOLD  5452  copsexgw  5501  copsexg  5502  elopab  5537  elopabrOLD  5573  0nelelxp  5724  elvvuni  5765  optocl  5783  relopabiALT  5836  relop  5864  elreldm  5949  xpnz  6181  xpdifid  6190  dfco2a  6268  unielrel  6296  unixp0  6305  funsndifnop  7171  fmptsng  7188  oprabidw  7462  oprabid  7463  oprabv  7493  1stval2  8030  2ndval2  8031  1st2val  8041  2nd2val  8042  xp1st  8045  xp2nd  8046  frxp  8150  poxp  8152  soxp  8153  rntpos  8263  dftpos4  8269  tpostpos  8270  frrlem4  8313  wfrlem4OLD  8351  wfrfunOLD  8358  tfrlem7  8422  ener  9040  domtr  9046  unen  9085  xpsnen  9094  undom  9098  sbthlem10  9131  mapen  9180  cnvfi  9215  entrfil  9223  domtrfil  9230  sbthfilem  9236  djuunxp  9959  fseqen  10065  dfac5lem4  10164  dfac5lem4OLD  10166  kmlem16  10204  axdc4lem  10493  hashfacen  14490  hashle2pr  14513  fundmge2nop0  14538  catcone0  17732  gictr  19307  dvdsrval  20378  rngqiprngimfo  21329  thlle  21734  thlleOLD  21735  hmphtr  23807  fsumdvdsmul  27253  griedg0ssusgr  29297  rgrusgrprc  29622  numclwwlk1lem2fo  30387  frgrregord013  30424  friendship  30428  nvss  30622  spanuni  31573  5oalem7  31689  3oalem3  31693  opabssi  32633  gsummpt2co  33034  qqhval2  33945  bnj605  34900  bnj607  34909  funen1cnv  35081  fineqvac  35090  loop1cycl  35122  satfv1  35348  sat1el2xp  35364  fmla0xp  35368  satefvfmla0  35403  mppspstlem  35556  mppsval  35557  pprodss4v  35866  sscoid  35895  colinearex  36042  copsex2b  37123  rictr  42507  pr2cv  43538  stoweidlem35  45991  funop1  47233  sprsymrelfvlem  47415  grictr  47830  uspgrsprf  47990  uspgrsprf1  47991  rrx2plordisom  48573