Theorem exlimivv 1936

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

Syntax hints:   → wi 4  ∃wex 1782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-ex 1783

This theorem is referenced by:  cgsex2g  3476  cgsex4g  3477  cgsex4gOLD  3478  opabss  5139  dtruALT2  5294  dtru  5360  copsexgw  5405  copsexg  5406  elopab  5441  elopabrOLD  5477  0nelelxp  5625  elvvuni  5664  optocl  5682  relopabiALT  5735  relop  5762  elreldm  5847  xpnz  6067  xpdifid  6076  dfco2a  6154  unielrel  6181  unixp0  6190  funsndifnop  7032  fmptsng  7049  oprabidw  7315  oprabid  7316  oprabv  7344  1stval2  7857  2ndval2  7858  1st2val  7868  2nd2val  7869  xp1st  7872  xp2nd  7873  frxp  7976  poxp  7978  soxp  7979  rntpos  8064  dftpos4  8070  tpostpos  8071  frrlem4  8114  wfrlem4OLD  8152  wfrfunOLD  8159  tfrlem7  8223  ener  8796  domtr  8802  unen  8845  xpsnen  8851  undom  8855  sbthlem10  8888  mapen  8937  cnvfi  8972  entrfil  8980  domtrfil  8987  sbthfilem  8993  djuunxp  9688  fseqen  9792  dfac5lem4  9891  kmlem16  9930  axdc4lem  10220  hashfacen  14175  hashfacenOLD  14176  hashle2pr  14200  fundmge2nop0  14215  catcone0  17405  gictr  18900  dvdsrval  19896  thlle  20912  thlleOLD  20913  hmphtr  22943  griedg0ssusgr  27641  rgrusgrprc  27965  numclwwlk1lem2fo  28731  frgrregord013  28768  friendship  28772  nvss  28964  spanuni  29915  5oalem7  30031  3oalem3  30035  opabssi  30962  gsummpt2co  31317  qqhval2  31941  bnj605  32896  bnj607  32905  funen1cnv  33069  fineqvac  33075  loop1cycl  33108  satfv1  33334  sat1el2xp  33350  fmla0xp  33354  satefvfmla0  33389  mppspstlem  33542  mppsval  33543  pprodss4v  34195  sscoid  34224  colinearex  34371  bj-dtru  35008  copsex2b  35320  sn-dtru  40195  pr2cv  41162  stoweidlem35  43583  funop1  44786  sprsymrelfvlem  44953  uspgrsprf  45319  uspgrsprf1  45320  rrx2plordisom  46080