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  3511  cgsex4g  3512  cgsex4gOLD  3513  opabss  5189  dtruALT2  5352  exneq  5422  dtruOLD  5428  copsexgw  5477  copsexg  5478  elopab  5514  elopabrOLD  5550  0nelelxp  5702  elvvuni  5744  optocl  5762  relopabiALT  5815  relop  5843  elreldm  5928  xpnz  6161  xpdifid  6170  dfco2a  6248  unielrel  6276  unixp0  6285  funsndifnop  7152  fmptsng  7171  oprabidw  7445  oprabid  7446  oprabv  7476  1stval2  8014  2ndval2  8015  1st2val  8025  2nd2val  8026  xp1st  8029  xp2nd  8030  frxp  8134  poxp  8136  soxp  8137  rntpos  8247  dftpos4  8253  tpostpos  8254  frrlem4  8297  wfrlem4OLD  8335  wfrfunOLD  8342  tfrlem7  8406  ener  9024  domtr  9030  unen  9069  xpsnen  9078  undom  9082  sbthlem10  9115  mapen  9164  cnvfi  9199  entrfil  9208  domtrfil  9215  sbthfilem  9221  djuunxp  9944  fseqen  10050  dfac5lem4  10149  dfac5lem4OLD  10151  kmlem16  10189  axdc4lem  10478  hashfacen  14476  hashle2pr  14499  fundmge2nop0  14524  catcone0  17706  gictr  19268  dvdsrval  20334  rngqiprngimfo  21278  thlle  21683  thlleOLD  21684  hmphtr  23756  fsumdvdsmul  27193  griedg0ssusgr  29229  rgrusgrprc  29554  numclwwlk1lem2fo  30324  frgrregord013  30361  friendship  30365  nvss  30559  spanuni  31510  5oalem7  31626  3oalem3  31630  opabssi  32572  gsummpt2co  32997  qqhval2  33924  bnj605  34862  bnj607  34871  funen1cnv  35043  fineqvac  35052  loop1cycl  35083  satfv1  35309  sat1el2xp  35325  fmla0xp  35329  satefvfmla0  35364  mppspstlem  35517  mppsval  35518  pprodss4v  35826  sscoid  35855  colinearex  36002  copsex2b  37082  rictr  42475  pr2cv  43506  stoweidlem35  45995  funop1  47241  sprsymrelfvlem  47423  grictr  47838  uspgrsprf  48008  uspgrsprf1  48009  rrx2plordisom  48590