Theorem rexlimdvv 3194

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 3137	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∃𝑦 ∈ 𝐵 𝜓 → 𝜒))
4	3	rexlimdva 3139	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 → 𝜒))

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-rex 3063

This theorem is referenced by:  rexlimdvva  3195  fprb  7142  f1oiso2  7300  omeu  8513  xpdom2  9003  rex2dom  9156  elfiun  9336  rankxplim3  9796  brdom6disj  10445  fpwwe2lem11  10555  tskxpss  10686  genpss  10918  genpcd  10920  genpnmax  10921  distrlem1pr  10939  distrlem5pr  10941  ltexprlem6  10955  reclem4pr  10964  supadd  12115  supmullem1  12117  supmullem2  12118  qaddcl  12906  qmulcl  12908  01sqrexlem6  15200  caubnd  15312  summo  15670  bezoutlem3  16501  bezoutlem4  16502  dvdsgcd  16504  gcddiv  16511  pceu  16808  pcqcl  16818  symgpssefmnd  19362  lspfixed  21118  lspexch  21119  lsmcv  21131  lspsolvlem  21132  hausnei2  23328  uncmp  23378  txcnp  23595  tx1stc  23625  fbasrn  23859  rnelfmlem  23927  blssps  24399  blss  24400  tgqioo  24775  ovolunlem2  25475  2sqnn  27416  madebdayim  27894  ax5seg  29021  axpasch  29024  axeuclid  29046  upgredg2vtx  29224  pjhthmo  31388  shmodsi  31475  pjpjpre  31505  chscllem4  31726  sumdmdlem  32504  cdj3lem2a  32522  cdj3lem2b  32523  cdj3lem3a  32525  dya2iocnrect  34441  satffunlem2lem1  35602  btwndiff  36225  btwnconn1lem13  36297  btwnconn1lem14  36298  brsegle  36306  segletr  36312  segleantisym  36313  nn0prpwlem  36520  ismblfin  37996  heibor1lem  38144  crngohomfo  38341  lsmsat  39468  3dim1  39927  3dim3  39929  1cvratex  39933  atcvrlln2  39979  atcvrlln  39980  lplnnlelln  40003  llncvrlpln2  40017  lplnexllnN  40024  2llnjN  40027  lvolnlelln  40044  lvolnlelpln  40045  lplncvrlvol2  40075  2lplnj  40080  lneq2at  40238  lnatexN  40239  lncvrat  40242  lncmp  40243  paddasslem15  40294  paddasslem16  40295  pmodlem2  40307  pmapjoin  40312  llnexchb2  40329  lhp2lt  40461  cdlemf  41023  cdlemg1cex  41048  cdlemg2ce  41052  cdlemn11pre  41670  dihord2pre  41685  dihord4  41718  dihmeetlem20N  41786  mapdpglem24  42164  mapdpglem32  42165  baerlem3lem2  42170  baerlem5alem2  42171  baerlem5blem2  42172  hdmapglem7  42389  sn-addlid  42850  rexlimdv3d  43129  mzpcompact2lem  43197  pellex  43281  onexomgt  43687  onexoegt  43690  oaun3lem1  43820  oaun3lem2  43821  disjrnmpt2  45636  mullimc  46064  mullimcf  46071  addlimc  46094  limclner  46097  fourierdlem42  46595  fourierdlem80  46632  fourierdlem97  46649  sge0resplit  46852  volicorescl  46999  opnvonmbllem2  47079  smfaddlem1  47209  smflimlem6  47222  gbepos  48246  gbowpos  48247  gbegt5  48249  gboge9  48252  isuspgrimlem  48383  usgrgrtrirex  48438  isubgr3stgrlem6  48459  gpgcubic  48567  gpg5nbgr3star  48569  pgnbgreunbgrlem3  48606  pgnbgreunbgrlem6  48612  pgnbgreunbgr  48613  seposep  49413  iscnrm3lem6  49425