Theorem exlimivv 1929

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

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

This theorem is referenced by:  cgsex2g  3538  cgsex4g  3539  opabss  5122  dtru  5263  copsexgw  5373  copsexg  5374  elopab  5406  elopabr  5439  epelgOLD  5461  0nelelxp  5584  elvvuni  5622  optocl  5639  relopabiALT  5689  relop  5715  elreldm  5799  xpnz  6010  xpdifid  6019  dfco2a  6093  unielrel  6119  unixp0  6128  funsndifnop  6907  fmptsng  6924  oprabidw  7181  oprabid  7182  oprabv  7208  1stval2  7700  2ndval2  7701  1st2val  7711  2nd2val  7712  xp1st  7715  xp2nd  7716  frxp  7814  poxp  7816  soxp  7817  rntpos  7899  dftpos4  7905  tpostpos  7906  wfrlem4  7952  wfrfun  7959  tfrlem7  8013  ener  8550  domtr  8556  unen  8590  xpsnen  8595  sbthlem10  8630  mapen  8675  djuunxp  9344  fseqen  9447  dfac5lem4  9546  kmlem16  9585  axdc4lem  9871  hashfacen  13806  hashle2pr  13829  fundmge2nop0  13844  gictr  18409  dvdsrval  19389  thlle  20835  hmphtr  22385  griedg0ssusgr  27041  rgrusgrprc  27365  numclwwlk1lem2fo  28131  frgrregord013  28168  friendship  28172  nvss  28364  spanuni  29315  5oalem7  29431  3oalem3  29435  opabssi  30358  gsummpt2co  30681  qqhval2  31218  bnj605  32174  bnj607  32183  funen1cnv  32352  loop1cycl  32379  satfv1  32605  sat1el2xp  32621  fmla0xp  32625  satefvfmla0  32660  mppspstlem  32813  mppsval  32814  frrlem4  33121  pprodss4v  33340  sscoid  33369  colinearex  33516  bj-dtru  34134  copsex2b  34426  sn-dtru  39104  pr2cv  39900  stoweidlem35  42314  funop1  43476  sprsymrelfvlem  43646  uspgrsprf  44015  uspgrsprf1  44016  rrx2plordisom  44704