Theorem rexlimdvva 3294

Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 18-Jun-2014.)

Hypothesis

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

Assertion

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

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

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

Proof of Theorem rexlimdvva

Step	Hyp	Ref	Expression
1		rexlimdvva.1	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 → 𝜒))
2	1	ex 415	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝜓 → 𝜒)))
3	2	rexlimdvv 3293	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 → 𝜒))

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2114  ∃wrex 3139

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 209  df-an 399  df-ex 1781  df-ral 3143  df-rex 3144

This theorem is referenced by:  disjxiun  5063  reuop  6144  f1prex  7040  f1o2ndf1  7818  uniinqs  8377  eroveu  8392  eroprf  8395  ralxpmap  8460  unxpdomlem3  8724  finsschain  8831  dffi3  8895  sornom  9699  genpv  10421  genpdm  10424  1re  10641  cnegex  10821  zaddcl  12023  rexanre  14706  o1lo1  14894  lo1resb  14921  o1resb  14923  rlimcn2  14947  climcn2  14949  o1of2  14969  o1rlimmul  14975  lo1add  14983  lo1mul  14984  summo  15074  o1fsum  15168  ntrivcvgmul  15258  prodmolem2  15289  prodmo  15290  dvds2lem  15622  bezoutlem4  15890  dvdsmulgcd  15905  divgcdcoprm0  16009  cncongr1  16011  pcqmul  16190  pcneg  16210  pcadd  16225  4sqlem1  16284  4sqlem2  16285  4sqlem4  16288  mul4sq  16290  4sqlem12  16292  4sqlem13  16293  4sqlem18  16298  vdwmc2  16315  vdwlem7  16323  vdwlem9  16325  vdwlem10  16326  vdwlem11  16327  ramlb  16355  ramub1lem2  16363  imasaddfnlem  16801  imasmnd2  17948  imasgrp2  18214  cyccom  18346  gaorber  18438  psgnunilem2  18623  psgneu  18634  lsmsubm  18778  lsmsubg  18779  lsmmod  18801  lsmdisj2  18808  pj1eu  18822  efgtlen  18852  efgredlem  18873  efgredeu  18878  efgcpbllemb  18881  frgpuptinv  18897  frgpup3lem  18903  qusabl  18985  frgpnabllem1  18993  frgpnabl  18995  cygablOLD  19011  dprdsubg  19146  ablfacrp  19188  pgpfac1lem3  19199  imasring  19369  dvdsrtr  19402  lss1d  19735  lsmcl  19855  lsmelval2  19857  lbsextlem2  19931  isnzr2  20036  qsssubdrg  20604  znfld  20707  cygznlem3  20716  psgnghm  20724  lsmcss  20836  mdetunilem7  21227  mdetunilem8  21228  cayleyhamilton0  21497  cayleyhamiltonALT  21499  restbas  21766  ordtbas2  21799  ordtbas  21800  cnhaus  21962  cldllycmp  22103  txbas  22175  ptbasin  22185  txcls  22212  xkoccn  22227  txindis  22242  txlly  22244  txnlly  22245  pthaus  22246  ptrescn  22247  txhaus  22255  tx1stc  22258  txkgen  22260  xkohaus  22261  xkoptsub  22262  xkopt  22263  xkoco1cn  22265  xkoco2cn  22266  xkoinjcn  22295  fmfnfmlem3  22564  fmfnfmlem4  22565  hausflimi  22588  hauspwpwf1  22595  txflf  22614  qustgplem  22729  blin2  23039  prdsxmslem2  23139  xrge0tsms  23442  addcnlem  23472  minveclem3b  24031  pmltpc  24051  evthicc2  24061  dyaddisj  24197  ismbfd  24240  mbfimaopnlem  24256  rolle  24587  dvcnvrelem1  24614  dvcvx  24617  itgsubst  24646  plyf  24788  plypf1  24802  plyadd  24807  plymul  24808  coeeu  24815  dgrlem  24819  coeid  24828  aalioulem6  24926  logbgcd1irr  25372  o1cxp  25552  dchrptlem2  25841  lgsdchr  25931  2sqlem5  25998  2sqlem9  26003  2sqb  26008  2sqreulem1  26022  2sqreunnlem1  26025  2sqreunnltblem  26027  pntlemp  26186  pnt3  26188  ostthlem1  26203  ostth3  26214  axcontlem4  26753  axcontlem9  26758  upgrpredgv  26924  edglnl  26928  numedglnl  26929  usgredg4  26999  nbuhgr2vtx1edgb  27134  2pthon3v  27722  umgr3v3e3cycl  27963  3cyclfrgr  28067  n4cyclfrgr  28070  frgrwopreg  28102  2clwwlk2clwwlk  28129  ubthlem3  28649  cdjreui  30209  cdj3i  30218  br8d  30361  xrofsup  30492  xrge0tsmsd  30692  qqhval2  31223  mbfmco2  31523  txpconn  32479  cvmlift2lem10  32559  cvmlift2lem12  32561  cvmlift3lem7  32572  cvmlift3lem8  32573  satfv0  32605  satfv0fun  32618  satffunlem2lem1  32651  mclsppslem  32830  br8  32992  br6  32993  br4  32994  frrlem9  33131  noprefixmo  33202  brsegle  33569  tailfb  33725  unbdqndv2  33850  mblfinlem3  34946  ismblfin  34948  itg2addnc  34961  ftc1anc  34990  isbnd2  35076  isbnd3  35077  ssbnd  35081  ispridlc  35363  lshpkrlem6  36266  athgt  36607  3dim1  36618  3dim2  36619  lvolex3N  36689  llncvrlpln2  36708  lplncvrlvol2  36766  linepsubN  36903  lncvrelatN  36932  linepsubclN  37102  eldioph2  39408  eldioph2b  39409  diophin  39418  diophun  39419  fphpdo  39463  irrapxlem3  39470  irrapxlem5  39472  pell1234qrne0  39499  pell1234qrreccl  39500  pell1234qrmulcl  39501  pell14qrgt0  39505  pell14qrdich  39515  pell1qrge1  39516  pell1qrgap  39520  pellqrex  39525  rmxycomplete  39563  jm2.27  39654  stoweidlem49  42383  ichreuopeq  43684  prproropf1olem2  43715  prproropf1olem4  43717  paireqne  43722  reupr  43733  requad2  43837  gbowgt5  43976  isomuspgrlem1  44041  isomuspgrlem2b  44043  isomuspgrlem2d  44045  m1modmmod  44630  prelrrx2b  44750