Theorem rexlimdvva 3205

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2098  ∃wrex 3064

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 396  df-ex 1774  df-rex 3065

This theorem is referenced by:  disjxiun  5138  reuop  6286  f1prex  7278  f1o2ndf1  8108  poxp2  8129  xpord2pred  8131  sexp2  8132  xpord3pred  8138  sexp3  8139  frrlem9  8280  uniinqs  8793  eroveu  8808  eroprf  8811  ralxpmap  8892  unxpdomlem3  9254  finsschain  9361  dffi3  9428  sornom  10274  genpv  10996  genpdm  10999  1re  11218  cnegex  11399  zaddcl  12606  rexanre  15299  o1lo1  15487  lo1resb  15514  o1resb  15516  rlimcn3  15540  climcn2  15543  o1of2  15563  o1rlimmul  15569  lo1add  15577  lo1mul  15578  summo  15669  o1fsum  15765  ntrivcvgmul  15854  prodmolem2  15885  prodmo  15886  dvds2lem  16219  bezoutlem4  16491  dvdsmulgcd  16504  divgcdcoprm0  16609  cncongr1  16611  pcqmul  16795  pcneg  16816  pcadd  16831  4sqlem1  16890  4sqlem2  16891  4sqlem4  16894  mul4sq  16896  4sqlem12  16898  4sqlem13  16899  4sqlem18  16904  vdwmc2  16921  vdwlem7  16929  vdwlem9  16931  vdwlem10  16932  vdwlem11  16933  ramlb  16961  ramub1lem2  16969  imasaddfnlem  17483  imasmnd2  18704  xpsmnd0  18708  imasgrp2  18983  cyccom  19129  gaorber  19224  psgnunilem2  19415  psgneu  19426  lsmsubm  19573  lsmsubg  19574  lsmmod  19595  lsmdisj2  19602  pj1eu  19616  efgtlen  19646  efgredlem  19667  efgredeu  19672  efgcpbllemb  19675  frgpuptinv  19691  frgpup3lem  19697  qusabl  19785  frgpnabllem1  19793  frgpnabl  19795  dprdsubg  19946  ablfacrp  19988  pgpfac1lem3  19999  imasrng  20082  imasring  20229  xpsring1d  20232  dvdsrtr  20270  isnzr2  20420  lss1d  20810  lsmcl  20931  lsmelval2  20933  lbsextlem2  21010  qsssubdrg  21320  znfld  21455  cygznlem3  21464  psgnghm  21473  lsmcss  21585  mdetunilem7  22475  mdetunilem8  22476  cayleyhamilton0  22746  cayleyhamiltonALT  22748  restbas  23017  ordtbas2  23050  ordtbas  23051  cnhaus  23213  cldllycmp  23354  txbas  23426  ptbasin  23436  txcls  23463  xkoccn  23478  txindis  23493  txlly  23495  txnlly  23496  pthaus  23497  ptrescn  23498  txhaus  23506  tx1stc  23509  txkgen  23511  xkohaus  23512  xkoptsub  23513  xkopt  23514  xkoco1cn  23516  xkoco2cn  23517  xkoinjcn  23546  fmfnfmlem3  23815  fmfnfmlem4  23816  hausflimi  23839  hauspwpwf1  23846  txflf  23865  qustgplem  23980  blin2  24290  prdsxmslem2  24393  xrge0tsms  24705  addcnlem  24735  minveclem3b  25311  pmltpc  25334  evthicc2  25344  dyaddisj  25480  ismbfd  25523  mbfimaopnlem  25539  rolle  25877  dvcnvrelem1  25905  dvcvx  25908  itgsubst  25939  plyf  26087  plypf1  26101  plyadd  26106  plymul  26107  coeeu  26114  dgrlem  26118  coeid  26127  aalioulem6  26227  logbgcd1irr  26681  o1cxp  26862  dchrptlem2  27153  lgsdchr  27243  2sqlem5  27310  2sqlem9  27315  2sqb  27320  2sqreulem1  27334  2sqreunnlem1  27337  2sqreunnltblem  27339  pntlemp  27498  pnt3  27500  ostthlem1  27515  ostth3  27526  nosupprefixmo  27588  noinfprefixmo  27589  addsproplem2  27842  negsproplem2  27896  mulsproplem9  27979  ssltmul1  28002  ssltmul2  28003  precsexlem8  28067  precsexlem9  28068  precsexlem10  28069  precsexlem11  28070  recut  28179  readdscl  28182  remulscl  28185  axcontlem4  28733  axcontlem9  28738  upgrpredgv  28907  edglnl  28911  numedglnl  28912  usgredg4  28982  nbuhgr2vtx1edgb  29117  2pthon3v  29706  umgr3v3e3cycl  29946  3cyclfrgr  30050  n4cyclfrgr  30053  frgrwopreg  30085  2clwwlk2clwwlk  30112  ubthlem3  30634  cdjreui  32194  cdj3i  32203  br8d  32348  xrofsup  32487  xrge0tsmsd  32715  qqhval2  33492  mbfmco2  33794  txpconn  34751  cvmlift2lem10  34831  cvmlift2lem12  34833  cvmlift3lem7  34844  cvmlift3lem8  34845  satfv0  34877  satfv0fun  34890  satffunlem2lem1  34923  mclsppslem  35102  br8  35259  br6  35260  br4  35261  brsegle  35613  tailfb  35770  unbdqndv2  35895  mblfinlem3  37040  ismblfin  37042  itg2addnc  37055  ftc1anc  37082  isbnd2  37164  isbnd3  37165  ssbnd  37169  ispridlc  37451  lshpkrlem6  38498  athgt  38840  3dim1  38851  3dim2  38852  lvolex3N  38922  llncvrlpln2  38941  lplncvrlvol2  38999  linepsubN  39136  lncvrelatN  39165  linepsubclN  39335  fsuppind  41724  sn-negex12  41872  flt4lem7  41984  nna4b4nsq  41985  eldioph2  42083  eldioph2b  42084  diophin  42093  diophun  42094  fphpdo  42138  irrapxlem3  42145  irrapxlem5  42147  pell1234qrne0  42174  pell1234qrreccl  42175  pell1234qrmulcl  42176  pell14qrgt0  42180  pell14qrdich  42190  pell1qrge1  42191  pell1qrgap  42195  pellqrex  42200  rmxycomplete  42239  jm2.27  42330  stoweidlem49  45342  ichreuopeq  46718  prproropf1olem2  46749  prproropf1olem4  46751  paireqne  46756  reupr  46767  requad2  46868  gbowgt5  47007  isomuspgrlem1  47072  isomuspgrlem2b  47074  isomuspgrlem2d  47076  m1modmmod  47487  prelrrx2b  47680