Theorem rexlimdvv 3221

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2145  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-rex 3090

This theorem is referenced by:  rexlimdvva  3222  fprb  7182  f1oiso2  7340  omeu  8558  xpdom2  9048  rex2dom  9201  elfiun  9378  rankxplim3  9841  brdom6disj  10504  fpwwe2lem11  10614  tskxpss  10745  genpss  10977  genpcd  10979  genpnmax  10980  distrlem1pr  10998  distrlem5pr  11000  ltexprlem6  11014  reclem4pr  11023  supadd  12171  supmullem1  12173  supmullem2  12174  qaddcl  12977  qmulcl  12979  01sqrexlem6  15286  caubnd  15398  summo  15756  bezoutlem3  16587  bezoutlem4  16588  dvdsgcd  16590  gcddiv  16597  pceu  16894  pcqcl  16904  symgpssefmnd  19454  lspfixed  21218  lspexch  21219  lsmcv  21231  lspsolvlem  21232  hausnei2  23467  uncmp  23517  txcnp  23734  tx1stc  23764  fbasrn  23998  rnelfmlem  24066  blssps  24538  blss  24539  tgqioo  24914  ovolunlem2  25614  2sqnn  27557  madebdayim  28035  ax5seg  29193  axpasch  29196  axeuclid  29218  upgredg2vtx  29396  pjhthmo  31559  shmodsi  31646  pjpjpre  31676  chscllem4  31897  sumdmdlem  32675  cdj3lem2a  32693  cdj3lem2b  32694  cdj3lem3a  32696  dya2iocnrect  34583  satffunlem2lem1  35762  btwndiff  36385  btwnconn1lem13  36457  btwnconn1lem14  36458  brsegle  36466  segletr  36472  segleantisym  36473  nn0prpwlem  36690  ismblfin  38167  heibor1lem  38315  crngohomfo  38512  lsmsat  39639  3dim1  40098  3dim3  40100  1cvratex  40104  atcvrlln2  40150  atcvrlln  40151  lplnnlelln  40174  llncvrlpln2  40188  lplnexllnN  40195  2llnjN  40198  lvolnlelln  40215  lvolnlelpln  40216  lplncvrlvol2  40246  2lplnj  40251  lneq2at  40409  lnatexN  40410  lncvrat  40413  lncmp  40414  paddasslem15  40465  paddasslem16  40466  pmodlem2  40478  pmapjoin  40483  llnexchb2  40500  lhp2lt  40632  cdlemf  41194  cdlemg1cex  41219  cdlemg2ce  41223  cdlemn11pre  41841  dihord2pre  41856  dihord4  41889  dihmeetlem20N  41957  mapdpglem24  42335  mapdpglem32  42336  baerlem3lem2  42341  baerlem5alem2  42342  baerlem5blem2  42343  hdmapglem7  42560  sn-addlid  43020  rexlimdv3d  43271  mzpcompact2lem  43339  pellex  43419  onexomgt  43825  onexoegt  43828  oaun3lem1  43958  oaun3lem2  43959  disjrnmpt2  45765  mullimc  46191  mullimcf  46198  addlimc  46221  limclner  46224  fourierdlem42  46722  fourierdlem80  46759  fourierdlem97  46776  sge0resplit  46979  volicorescl  47126  opnvonmbllem2  47206  smfaddlem1  47336  smflimlem6  47349  gbepos  48379  gbowpos  48380  gbegt5  48382  gboge9  48385  isuspgrimlem  48516  usgrgrtrirex  48571  isubgr3stgrlem6  48592  gpgcubic  48700  gpg5nbgr3star  48702  pgnbgreunbgrlem3  48739  pgnbgreunbgrlem6  48745  pgnbgreunbgr  48746  seposep  49556  iscnrm3lem6  49568