Theorem rexlimdvva 3202

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 411	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝜓 → 𝜒)))
3	2	rexlimdvv 3201	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 → 𝜒))

Syntax hints:   → wi 4   ∧ wa 394   ∈ wcel 2098  ∃wrex 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-rex 3061

This theorem is referenced by:  disjxiun  5140  reuop  6292  f1prex  7288  f1o2ndf1  8123  poxp2  8144  xpord2pred  8146  sexp2  8147  xpord3pred  8153  sexp3  8154  frrlem9  8296  uniinqs  8812  eroveu  8827  eroprf  8830  ralxpmap  8911  unxpdomlem3  9273  finsschain  9381  dffi3  9452  sornom  10298  genpv  11020  genpdm  11023  1re  11242  cnegex  11423  zaddcl  12630  rexanre  15323  o1lo1  15511  lo1resb  15538  o1resb  15540  rlimcn3  15564  climcn2  15567  o1of2  15587  o1rlimmul  15593  lo1add  15601  lo1mul  15602  summo  15693  o1fsum  15789  ntrivcvgmul  15878  prodmolem2  15909  prodmo  15910  dvds2lem  16243  bezoutlem4  16515  dvdsmulgcd  16528  divgcdcoprm0  16633  cncongr1  16635  pcqmul  16819  pcneg  16840  pcadd  16855  4sqlem1  16914  4sqlem2  16915  4sqlem4  16918  mul4sq  16920  4sqlem12  16922  4sqlem13  16923  4sqlem18  16928  vdwmc2  16945  vdwlem7  16953  vdwlem9  16955  vdwlem10  16956  vdwlem11  16957  ramlb  16985  ramub1lem2  16993  imasaddfnlem  17507  imasmnd2  18728  xpsmnd0  18732  imasgrp2  19013  cyccom  19160  gaorber  19261  psgnunilem2  19452  psgneu  19463  lsmsubm  19610  lsmsubg  19611  lsmmod  19632  lsmdisj2  19639  pj1eu  19653  efgtlen  19683  efgredlem  19704  efgredeu  19709  efgcpbllemb  19712  frgpuptinv  19728  frgpup3lem  19734  qusabl  19822  frgpnabllem1  19830  frgpnabl  19832  dprdsubg  19983  ablfacrp  20025  pgpfac1lem3  20036  imasrng  20119  imasring  20268  xpsring1d  20271  dvdsrtr  20309  isnzr2  20459  lss1d  20849  lsmcl  20970  lsmelval2  20972  lbsextlem2  21049  qsssubdrg  21361  znfld  21496  cygznlem3  21505  psgnghm  21514  lsmcss  21626  psdmul  22096  mdetunilem7  22536  mdetunilem8  22537  cayleyhamilton0  22807  cayleyhamiltonALT  22809  restbas  23078  ordtbas2  23111  ordtbas  23112  cnhaus  23274  cldllycmp  23415  txbas  23487  ptbasin  23497  txcls  23524  xkoccn  23539  txindis  23554  txlly  23556  txnlly  23557  pthaus  23558  ptrescn  23559  txhaus  23567  tx1stc  23570  txkgen  23572  xkohaus  23573  xkoptsub  23574  xkopt  23575  xkoco1cn  23577  xkoco2cn  23578  xkoinjcn  23607  fmfnfmlem3  23876  fmfnfmlem4  23877  hausflimi  23900  hauspwpwf1  23907  txflf  23926  qustgplem  24041  blin2  24351  prdsxmslem2  24454  xrge0tsms  24766  addcnlem  24796  minveclem3b  25372  pmltpc  25395  evthicc2  25405  dyaddisj  25541  ismbfd  25584  mbfimaopnlem  25600  rolle  25938  dvcnvrelem1  25966  dvcvx  25969  itgsubst  26000  plyf  26148  plypf1  26162  plyadd  26167  plymul  26168  coeeu  26175  dgrlem  26179  coeid  26188  aalioulem6  26288  logbgcd1irr  26742  o1cxp  26923  dchrptlem2  27214  lgsdchr  27304  2sqlem5  27371  2sqlem9  27376  2sqb  27381  2sqreulem1  27395  2sqreunnlem1  27398  2sqreunnltblem  27400  pntlemp  27559  pnt3  27561  ostthlem1  27576  ostth3  27587  nosupprefixmo  27649  noinfprefixmo  27650  addsproplem2  27903  negsproplem2  27957  mulsproplem9  28044  ssltmul1  28067  ssltmul2  28068  precsexlem8  28132  precsexlem9  28133  precsexlem10  28134  precsexlem11  28135  recut  28266  readdscl  28269  remulscl  28272  axcontlem4  28820  axcontlem9  28825  upgrpredgv  28994  edglnl  28998  numedglnl  28999  usgredg4  29072  nbuhgr2vtx1edgb  29207  2pthon3v  29796  umgr3v3e3cycl  30036  3cyclfrgr  30140  n4cyclfrgr  30143  frgrwopreg  30175  2clwwlk2clwwlk  30202  ubthlem3  30724  cdjreui  32284  cdj3i  32293  br8d  32443  xrofsup  32580  xrge0tsmsd  32814  qqhval2  33639  mbfmco2  33941  txpconn  34898  cvmlift2lem10  34978  cvmlift2lem12  34980  cvmlift3lem7  34991  cvmlift3lem8  34992  satfv0  35024  satfv0fun  35037  satffunlem2lem1  35070  mclsppslem  35249  br8  35406  br6  35407  br4  35408  brsegle  35760  tailfb  35917  unbdqndv2  36042  mblfinlem3  37188  ismblfin  37190  itg2addnc  37203  ftc1anc  37230  isbnd2  37312  isbnd3  37313  ssbnd  37317  ispridlc  37599  lshpkrlem6  38642  athgt  38984  3dim1  38995  3dim2  38996  lvolex3N  39066  llncvrlpln2  39085  lplncvrlvol2  39143  linepsubN  39280  lncvrelatN  39309  linepsubclN  39479  fsuppind  41887  sn-negex12  42035  flt4lem7  42147  nna4b4nsq  42148  eldioph2  42246  eldioph2b  42247  diophin  42256  diophun  42257  fphpdo  42301  irrapxlem3  42308  irrapxlem5  42310  pell1234qrne0  42337  pell1234qrreccl  42338  pell1234qrmulcl  42339  pell14qrgt0  42343  pell14qrdich  42353  pell1qrge1  42354  pell1qrgap  42358  pellqrex  42363  rmxycomplete  42402  jm2.27  42493  stoweidlem49  45499  ichreuopeq  46875  prproropf1olem2  46906  prproropf1olem4  46908  paireqne  46913  reupr  46924  requad2  47025  gbowgt5  47164  m1modmmod  47705  prelrrx2b  47898