Theorem rexlimdvva 3211

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  ∃wrex 3070

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 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-rex 3071

This theorem is referenced by:  disjxiun  5145  reuop  6292  f1prex  7284  f1o2ndf1  8110  poxp2  8131  xpord2pred  8133  sexp2  8134  xpord3pred  8140  sexp3  8141  frrlem9  8281  uniinqs  8793  eroveu  8808  eroprf  8811  ralxpmap  8892  unxpdomlem3  9254  finsschain  9361  dffi3  9428  sornom  10274  genpv  10996  genpdm  10999  1re  11216  cnegex  11397  zaddcl  12604  rexanre  15295  o1lo1  15483  lo1resb  15510  o1resb  15512  rlimcn3  15536  climcn2  15539  o1of2  15559  o1rlimmul  15565  lo1add  15573  lo1mul  15574  summo  15665  o1fsum  15761  ntrivcvgmul  15850  prodmolem2  15881  prodmo  15882  dvds2lem  16214  bezoutlem4  16486  dvdsmulgcd  16499  divgcdcoprm0  16604  cncongr1  16606  pcqmul  16788  pcneg  16809  pcadd  16824  4sqlem1  16883  4sqlem2  16884  4sqlem4  16887  mul4sq  16889  4sqlem12  16891  4sqlem13  16892  4sqlem18  16897  vdwmc2  16914  vdwlem7  16922  vdwlem9  16924  vdwlem10  16925  vdwlem11  16926  ramlb  16954  ramub1lem2  16962  imasaddfnlem  17476  imasmnd2  18664  xpsmnd0  18668  imasgrp2  18940  cyccom  19082  gaorber  19174  psgnunilem2  19365  psgneu  19376  lsmsubm  19523  lsmsubg  19524  lsmmod  19545  lsmdisj2  19552  pj1eu  19566  efgtlen  19596  efgredlem  19617  efgredeu  19622  efgcpbllemb  19625  frgpuptinv  19641  frgpup3lem  19647  qusabl  19735  frgpnabllem1  19743  frgpnabl  19745  dprdsubg  19896  ablfacrp  19938  pgpfac1lem3  19949  imasring  20147  xpsring1d  20150  dvdsrtr  20186  isnzr2  20301  lss1d  20579  lsmcl  20699  lsmelval2  20701  lbsextlem2  20778  qsssubdrg  21010  znfld  21122  cygznlem3  21131  psgnghm  21139  lsmcss  21251  mdetunilem7  22127  mdetunilem8  22128  cayleyhamilton0  22398  cayleyhamiltonALT  22400  restbas  22669  ordtbas2  22702  ordtbas  22703  cnhaus  22865  cldllycmp  23006  txbas  23078  ptbasin  23088  txcls  23115  xkoccn  23130  txindis  23145  txlly  23147  txnlly  23148  pthaus  23149  ptrescn  23150  txhaus  23158  tx1stc  23161  txkgen  23163  xkohaus  23164  xkoptsub  23165  xkopt  23166  xkoco1cn  23168  xkoco2cn  23169  xkoinjcn  23198  fmfnfmlem3  23467  fmfnfmlem4  23468  hausflimi  23491  hauspwpwf1  23498  txflf  23517  qustgplem  23632  blin2  23942  prdsxmslem2  24045  xrge0tsms  24357  addcnlem  24387  minveclem3b  24952  pmltpc  24974  evthicc2  24984  dyaddisj  25120  ismbfd  25163  mbfimaopnlem  25179  rolle  25514  dvcnvrelem1  25541  dvcvx  25544  itgsubst  25573  plyf  25719  plypf1  25733  plyadd  25738  plymul  25739  coeeu  25746  dgrlem  25750  coeid  25759  aalioulem6  25857  logbgcd1irr  26306  o1cxp  26486  dchrptlem2  26775  lgsdchr  26865  2sqlem5  26932  2sqlem9  26937  2sqb  26942  2sqreulem1  26956  2sqreunnlem1  26959  2sqreunnltblem  26961  pntlemp  27120  pnt3  27122  ostthlem1  27137  ostth3  27148  nosupprefixmo  27210  noinfprefixmo  27211  addsproplem2  27463  negsproplem2  27513  mulsproplem9  27590  ssltmul1  27612  ssltmul2  27613  precsexlem8  27670  precsexlem9  27671  precsexlem10  27672  precsexlem11  27673  axcontlem4  28263  axcontlem9  28268  upgrpredgv  28437  edglnl  28441  numedglnl  28442  usgredg4  28512  nbuhgr2vtx1edgb  28647  2pthon3v  29235  umgr3v3e3cycl  29475  3cyclfrgr  29579  n4cyclfrgr  29582  frgrwopreg  29614  2clwwlk2clwwlk  29641  ubthlem3  30163  cdjreui  31723  cdj3i  31732  br8d  31877  xrofsup  32018  xrge0tsmsd  32250  qqhval2  33031  mbfmco2  33333  txpconn  34292  cvmlift2lem10  34372  cvmlift2lem12  34374  cvmlift3lem7  34385  cvmlift3lem8  34386  satfv0  34418  satfv0fun  34431  satffunlem2lem1  34464  mclsppslem  34643  br8  34801  br6  34802  br4  34803  brsegle  35155  tailfb  35354  unbdqndv2  35479  mblfinlem3  36619  ismblfin  36621  itg2addnc  36634  ftc1anc  36661  isbnd2  36743  isbnd3  36744  ssbnd  36748  ispridlc  37030  lshpkrlem6  38077  athgt  38419  3dim1  38430  3dim2  38431  lvolex3N  38501  llncvrlpln2  38520  lplncvrlvol2  38578  linepsubN  38715  lncvrelatN  38744  linepsubclN  38914  fsuppind  41250  sn-negex12  41377  flt4lem7  41489  nna4b4nsq  41490  eldioph2  41588  eldioph2b  41589  diophin  41598  diophun  41599  fphpdo  41643  irrapxlem3  41650  irrapxlem5  41652  pell1234qrne0  41679  pell1234qrreccl  41680  pell1234qrmulcl  41681  pell14qrgt0  41685  pell14qrdich  41695  pell1qrge1  41696  pell1qrgap  41700  pellqrex  41705  rmxycomplete  41744  jm2.27  41835  stoweidlem49  44850  ichreuopeq  46226  prproropf1olem2  46257  prproropf1olem4  46259  paireqne  46264  reupr  46275  requad2  46376  gbowgt5  46515  isomuspgrlem1  46580  isomuspgrlem2b  46582  isomuspgrlem2d  46584  imasrng  46763  m1modmmod  47291  prelrrx2b  47484