Theorem exlimivv 1914

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

Syntax hints:   → wi 4  ∃wex 1765

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

This theorem depends on definitions:  df-bi 208  df-ex 1766

This theorem is referenced by:  cgsex2g  3484  cgsex4g  3485  opabss  5032  dtru  5169  copsexg  5280  elopab  5311  elopabr  5342  epelgOLD  5362  0nelelxp  5485  elvvuni  5521  optocl  5538  relopabiALT  5588  relop  5614  elreldm  5694  xpnz  5899  xpdifid  5908  dfco2a  5981  unielrel  6007  unixp0  6016  funsndifnop  6783  fmptsng  6800  oprabid  7054  oprabv  7080  1stval2  7569  2ndval2  7570  1st2val  7580  2nd2val  7581  xp1st  7584  xp2nd  7585  frxp  7680  poxp  7682  soxp  7683  rntpos  7763  dftpos4  7769  tpostpos  7770  wfrlem4  7816  wfrlem4OLD  7817  wfrfun  7824  tfrlem7  7878  ener  8411  domtr  8417  unen  8451  xpsnen  8455  sbthlem10  8490  mapen  8535  djuunxp  9203  fseqen  9306  dfac5lem4  9405  kmlem16  9444  axdc4lem  9730  hashfacen  13664  hashle2pr  13685  fundmge2nop0  13700  gictr  18160  dvdsrval  19089  thlle  20527  hmphtr  22079  griedg0ssusgr  26734  rgrusgrprc  27058  numclwwlk1lem2fo  27825  frgrregord013  27862  friendship  27866  nvss  28057  spanuni  29008  5oalem7  29124  3oalem3  29128  opabssi  30050  gsummpt2co  30491  qqhval2  30836  bnj605  31791  bnj607  31800  funen1cnv  31967  loop1cycl  31994  satfv1  32220  sat1el2xp  32236  fmla0xp  32240  satefvfmla0  32275  mppspstlem  32428  mppsval  32429  frrlem4  32737  pprodss4v  32956  sscoid  32985  colinearex  33132  bj-dtru  33710  sn-dtru  38662  pr2cv  39413  stoweidlem35  41884  funop1  43020  sprsymrelfvlem  43156  uspgrsprf  43525  uspgrsprf1  43526  rrx2plordisom  44213