Theorem rexlimdvva 3195

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 3194	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:  rexlimdvvva  3196  disjxiun  5097  reuop  6259  f1prex  7240  f1o2ndf1  8074  poxp2  8095  xpord2pred  8097  sexp2  8098  xpord3pred  8104  sexp3  8105  frrlem9  8246  uniinqs  8746  eroveu  8761  eroprf  8764  ralxpmap  8846  unxpdomlem3  9170  finsschain  9271  dffi3  9346  sornom  10199  genpv  10922  genpdm  10925  1re  11144  cnegex  11326  zaddcl  12543  rexanre  15282  o1lo1  15472  lo1resb  15499  o1resb  15501  rlimcn3  15525  climcn2  15528  o1of2  15548  o1rlimmul  15554  lo1add  15562  lo1mul  15563  summo  15652  o1fsum  15748  ntrivcvgmul  15837  prodmolem2  15870  prodmo  15871  dvds2lem  16207  bezoutlem4  16481  dvdsmulgcd  16495  divgcdcoprm0  16604  cncongr1  16606  pcqmul  16793  pcneg  16814  pcadd  16829  4sqlem1  16888  4sqlem2  16889  4sqlem4  16892  mul4sq  16894  4sqlem12  16896  4sqlem13  16897  4sqlem18  16902  vdwmc2  16919  vdwlem7  16927  vdwlem9  16929  vdwlem10  16930  vdwlem11  16931  ramlb  16959  ramub1lem2  16967  imasaddfnlem  17461  imasmnd2  18711  xpsmnd0  18715  imasgrp2  18997  cyccom  19144  gaorber  19249  psgnunilem2  19436  psgneu  19447  lsmsubm  19594  lsmsubg  19595  lsmmod  19616  lsmdisj2  19623  pj1eu  19637  efgtlen  19667  efgredlem  19688  efgredeu  19693  efgcpbllemb  19696  frgpuptinv  19712  frgpup3lem  19718  qusabl  19806  frgpnabllem1  19814  frgpnabl  19816  dprdsubg  19967  ablfacrp  20009  pgpfac1lem3  20020  imasrng  20124  imasring  20278  xpsring1d  20281  dvdsrtr  20316  isnzr2  20463  lss1d  20926  lsmcl  21047  lsmelval2  21049  lbsextlem2  21126  qsssubdrg  21393  znfld  21527  cygznlem3  21536  psgnghm  21547  lsmcss  21659  psdmul  22121  mdetunilem7  22574  mdetunilem8  22575  cayleyhamilton0  22845  cayleyhamiltonALT  22847  restbas  23114  ordtbas2  23147  ordtbas  23148  cnhaus  23310  cldllycmp  23451  txbas  23523  ptbasin  23533  txcls  23560  xkoccn  23575  txindis  23590  txlly  23592  txnlly  23593  pthaus  23594  ptrescn  23595  txhaus  23603  tx1stc  23606  txkgen  23608  xkohaus  23609  xkoptsub  23610  xkopt  23611  xkoco1cn  23613  xkoco2cn  23614  xkoinjcn  23643  fmfnfmlem3  23912  fmfnfmlem4  23913  hausflimi  23936  hauspwpwf1  23943  txflf  23962  qustgplem  24077  blin2  24385  prdsxmslem2  24485  xrge0tsms  24791  addcnlem  24821  minveclem3b  25396  pmltpc  25419  evthicc2  25429  dyaddisj  25565  ismbfd  25608  mbfimaopnlem  25624  rolle  25962  dvcnvrelem1  25990  dvcvx  25993  itgsubst  26024  plyf  26171  plypf1  26185  plyadd  26190  plymul  26191  coeeu  26198  dgrlem  26202  coeid  26211  aalioulem6  26313  logbgcd1irr  26772  o1cxp  26953  dchrptlem2  27244  lgsdchr  27334  2sqlem5  27401  2sqlem9  27406  2sqb  27411  2sqreulem1  27425  2sqreunnlem1  27428  2sqreunnltblem  27430  pntlemp  27589  pnt3  27591  ostthlem1  27606  ostth3  27617  nosupprefixmo  27680  noinfprefixmo  27681  addsproplem2  27978  negsproplem2  28037  mulsproplem9  28132  sltmuls1  28155  sltmuls2  28156  precsexlem8  28222  precsexlem9  28223  precsexlem10  28224  precsexlem11  28225  onmulscl  28286  eucliddivs  28384  zaddscl  28402  zmulscld  28405  z12addscl  28485  z12sge0  28491  recut  28502  readdscl  28507  remulscl  28510  axcontlem4  29052  axcontlem9  29057  upgrpredgv  29224  edglnl  29228  numedglnl  29229  usgredg4  29302  nbuhgr2vtx1edgb  29437  2pthon3v  30028  umgr3v3e3cycl  30271  3cyclfrgr  30375  n4cyclfrgr  30378  frgrwopreg  30410  2clwwlk2clwwlk  30437  ubthlem3  30959  cdjreui  32519  cdj3i  32528  br8d  32697  xrofsup  32857  xrge0tsmsd  33166  qqhval2  34159  mbfmco2  34442  txpconn  35445  cvmlift2lem10  35525  cvmlift2lem12  35527  cvmlift3lem7  35538  cvmlift3lem8  35539  satfv0  35571  satfv0fun  35584  satffunlem2lem1  35617  mclsppslem  35796  br8  35969  br6  35970  br4  35971  brsegle  36321  tailfb  36590  unbdqndv2  36730  mblfinlem3  37904  ismblfin  37906  itg2addnc  37919  ftc1anc  37946  isbnd2  38028  isbnd3  38029  ssbnd  38033  ispridlc  38315  lshpkrlem6  39485  athgt  39826  3dim1  39837  3dim2  39838  lvolex3N  39908  llncvrlpln2  39927  lplncvrlvol2  39985  linepsubN  40122  lncvrelatN  40151  linepsubclN  40321  sn-negex12  42781  fidomncyc  42899  fsuppind  42942  flt4lem7  43011  nna4b4nsq  43012  eldioph2  43113  eldioph2b  43114  diophin  43123  diophun  43124  fphpdo  43168  irrapxlem3  43175  irrapxlem5  43177  pell1234qrne0  43204  pell1234qrreccl  43205  pell1234qrmulcl  43206  pell14qrgt0  43210  pell14qrdich  43220  pell1qrge1  43221  pell1qrgap  43225  pellqrex  43230  rmxycomplete  43268  jm2.27  43359  stoweidlem49  46401  m1modmmod  47712  ichreuopeq  47827  prproropf1olem2  47858  prproropf1olem4  47860  paireqne  47865  reupr  47876  requad2  47977  gbowgt5  48116  isgrtri  48297  grimgrtri  48303  usgrgrtrirex  48304  gpgvtx0  48407  gpgvtx1  48408  gpgedgvtx0  48415  gpgedgvtx1  48416  pgn4cyclex  48480  prelrrx2b  49068