Theorem rexlimdvv 3189

Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 22-Jul-2004.)

Hypothesis

Ref	Expression
rexlimdvv.1	⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝜓 → 𝜒)))

Assertion

Ref	Expression
rexlimdvv	⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 → 𝜒))

Distinct variable groups:   𝑥,𝑦,𝜑   𝜒,𝑥,𝑦   𝑦,𝐴

Allowed substitution hints:   𝜓(𝑥,𝑦)   𝐴(𝑥)   𝐵(𝑥,𝑦)

Proof of Theorem rexlimdvv

Step	Hyp	Ref	Expression
1		rexlimdvv.1	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝜓 → 𝜒)))
2	1	expdimp 452	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ 𝐵 → (𝜓 → 𝜒)))
3	2	rexlimdv 3132	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∃𝑦 ∈ 𝐵 𝜓 → 𝜒))
4	3	rexlimdva 3134	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 → 𝜒))

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  ∃wrex 3057

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-rex 3058

This theorem is referenced by:  rexlimdvva  3190  fprb  7134  f1oiso2  7292  omeu  8506  xpdom2  8992  rex2dom  9144  elfiun  9321  rankxplim3  9781  brdom6disj  10430  fpwwe2lem11  10539  tskxpss  10670  genpss  10902  genpcd  10904  genpnmax  10905  distrlem1pr  10923  distrlem5pr  10925  ltexprlem6  10939  reclem4pr  10948  supadd  12097  supmullem1  12099  supmullem2  12100  qaddcl  12865  qmulcl  12867  01sqrexlem6  15156  caubnd  15268  summo  15626  bezoutlem3  16454  bezoutlem4  16455  dvdsgcd  16457  gcddiv  16464  pceu  16760  pcqcl  16770  symgpssefmnd  19310  lspfixed  21067  lspexch  21068  lsmcv  21080  lspsolvlem  21081  hausnei2  23269  uncmp  23319  txcnp  23536  tx1stc  23566  fbasrn  23800  rnelfmlem  23868  blssps  24340  blss  24341  tgqioo  24716  ovolunlem2  25427  2sqnn  27378  madebdayim  27834  ax5seg  28918  axpasch  28921  axeuclid  28943  upgredg2vtx  29121  pjhthmo  31284  shmodsi  31371  pjpjpre  31401  chscllem4  31622  sumdmdlem  32400  cdj3lem2a  32418  cdj3lem2b  32419  cdj3lem3a  32421  dya2iocnrect  34315  satffunlem2lem1  35469  btwndiff  36092  btwnconn1lem13  36164  btwnconn1lem14  36165  brsegle  36173  segletr  36179  segleantisym  36180  nn0prpwlem  36387  ismblfin  37721  heibor1lem  37869  crngohomfo  38066  lsmsat  39127  3dim1  39586  3dim3  39588  1cvratex  39592  atcvrlln2  39638  atcvrlln  39639  lplnnlelln  39662  llncvrlpln2  39676  lplnexllnN  39683  2llnjN  39686  lvolnlelln  39703  lvolnlelpln  39704  lplncvrlvol2  39734  2lplnj  39739  lneq2at  39897  lnatexN  39898  lncvrat  39901  lncmp  39902  paddasslem15  39953  paddasslem16  39954  pmodlem2  39966  pmapjoin  39971  llnexchb2  39988  lhp2lt  40120  cdlemf  40682  cdlemg1cex  40707  cdlemg2ce  40711  cdlemn11pre  41329  dihord2pre  41344  dihord4  41377  dihmeetlem20N  41445  mapdpglem24  41823  mapdpglem32  41824  baerlem3lem2  41829  baerlem5alem2  41830  baerlem5blem2  41831  hdmapglem7  42048  sn-addlid  42522  rexlimdv3d  42800  mzpcompact2lem  42868  pellex  42952  onexomgt  43358  onexoegt  43361  oaun3lem1  43491  oaun3lem2  43492  disjrnmpt2  45309  mullimc  45740  mullimcf  45747  addlimc  45770  limclner  45773  fourierdlem42  46271  fourierdlem80  46308  fourierdlem97  46325  sge0resplit  46528  volicorescl  46675  opnvonmbllem2  46755  smfaddlem1  46885  smflimlem6  46898  gbepos  47882  gbowpos  47883  gbegt5  47885  gboge9  47888  isuspgrimlem  48019  usgrgrtrirex  48074  isubgr3stgrlem6  48095  gpgcubic  48203  gpg5nbgr3star  48205  pgnbgreunbgrlem3  48242  pgnbgreunbgrlem6  48248  pgnbgreunbgr  48249  seposep  49050  iscnrm3lem6  49062