Theorem rexlimdvva 3220

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  ∃wrex 3087

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3088

This theorem is used by:  rexlimdvvva  3221  disjxiun  5100  reuop  6289  f1prex  7284  f1o2ndf1  8122  poxp2  8144  xpord2pred  8146  sexp2  8147  xpord3pred  8153  sexp3  8154  frrlem9  8296  uniinqs  8802  eroveu  8817  eroprf  8820  ralxpmap  8908  unxpdomlem3  9233  finsschain  9332  dffi3  9407  sornom  10336  genpv  11065  genpdm  11068  1re  11289  cnegex  11472  zaddcl  12717  rexanre  15494  o1lo1  15684  lo1resb  15711  o1resb  15713  rlimcn3  15737  climcn2  15740  o1of2  15760  o1rlimmul  15766  lo1add  15774  lo1mul  15775  summo  15863  o1fsum  15960  ntrivcvgmul  16051  prodmolem2  16082  prodmo  16083  dvds2lem  16418  bezoutlem4  16695  dvdsmulgcd  16710  divgcdcoprm0  16820  cncongr1  16822  pcqmul  17011  pcneg  17032  pcadd  17047  4sqlem1  17106  4sqlem2  17107  4sqlem4  17110  mul4sq  17112  4sqlem12  17114  4sqlem13  17115  4sqlem18  17120  vdwmc2  17137  vdwlem7  17145  vdwlem9  17147  vdwlem10  17148  vdwlem11  17149  ramlb  17177  ramub1lem2  17185  imasaddfnlem  17680  imasmnd2  18948  xpsmnd0  18952  imasgrp2  19245  cyccom  19398  gaorber  19502  psgnunilem2  19689  psgneu  19700  lsmsubm  19847  lsmsubg  19848  lsmmod  19869  lsmdisj2  19876  pj1eu  19890  efgtlen  19920  efgredlem  19941  efgredeu  19946  efgcpbllemb  19949  frgpuptinv  19965  frgpup3lem  19971  qusabl  20059  frgpnabllem1  20067  frgpnabl  20069  dprdsubg  20220  ablfacrp  20262  pgpfac1lem3  20273  imasrng  20379  imasring  20540  xpsring1d  20543  dvdsrtr  20578  isnzr2  20748  lss1d  21218  lsmcl  21338  lsmelval2  21340  lbsextlem2  21417  qsssubdrg  21712  znfld  21846  cygznlem3  21855  psgnghm  21866  lsmcss  21978  psdmul  22467  mdetunilem7  22913  mdetunilem8  22914  cayleyhamilton0  23187  cayleyhamiltonALT  23189  restbas  23456  ordtbas2  23489  ordtbas  23490  cnhaus  23652  cldllycmp  23794  txbas  23866  ptbasin  23876  txcls  23903  xkoccn  23918  txindis  23933  txlly  23935  txnlly  23936  pthaus  23937  ptrescn  23938  txhaus  23946  tx1stc  23949  txkgen  23951  xkohaus  23952  xkoptsub  23953  xkopt  23954  xkoco1cn  23956  xkoco2cn  23957  xkoinjcn  23986  fmfnfmlem3  24255  fmfnfmlem4  24256  hausflimi  24279  hauspwpwf1  24286  txflf  24305  qustgplem  24420  blin2  24728  prdsxmslem2  24828  xrge0tsms  25134  addcnlem  25164  minveclem3b  25729  pmltpc  25751  evthicc2  25761  dyaddisj  25897  ismbfd  25940  mbfimaopnlem  25956  rolle  26290  dvcnvrelem1  26317  dvcvx  26320  itgsubst  26349  plyf  26496  plypf1  26511  plyadd  26516  plymul  26517  coeeu  26524  dgrlem  26528  coeid  26537  aalioulem6  26646  logbgcd1irr  27104  o1cxp  27284  dchrptlem2  27574  lgsdchr  27664  2sqlem5  27731  2sqlem9  27736  2sqb  27741  2sqreulem1  27755  2sqreunnlem1  27758  2sqreunnltblem  27760  pntlemp  27919  pnt3  27921  ostthlem1  27936  ostth3  27947  flt4lem7  27971  nna4b4nsq  27972  nosupprefixmo  28039  noinfprefixmo  28040  addsproplem2  28338  negsproplem2  28397  mulsproplem9  28492  sltmuls1  28515  sltmuls2  28516  precsexlem8  28582  precsexlem9  28583  precsexlem10  28584  precsexlem11  28585  onmulscl  28646  eucliddivs  28744  zaddscl  28762  zmulscld  28765  z12addscl  28845  z12sge0  28851  recut  28862  readdscl  28867  remulscl  28870  axcontlem4  29527  axcontlem9  29532  upgrpredgv  29699  edglnl  29703  numedglnl  29704  usgredg4  29780  nbuhgr2vtx1edgb  29915  2pthon3v  30514  umgr3v3e3cycl  30767  3cyclfrgr  30871  n4cyclfrgr  30874  frgrwopreg  30906  2clwwlk2clwwlk  30933  ubthlem3  31456  cdjreui  33016  cdj3i  33025  br8d  33184  xrofsup  33341  xrge0tsmsd  33616  qqhval2  34596  mbfmco2  34880  txpconn  35966  cvmlift2lem10  36046  cvmlift2lem12  36048  cvmlift3lem7  36059  cvmlift3lem8  36060  satfv0  36092  satfv0fun  36105  satffunlem2lem1  36138  mclsppslem  36317  br8  36490  br6  36491  br4  36492  brsegle  36843  ltnmul  36935  nadddilem1  36939  tailfb  37135  unbdqndv2  37347  qdiff  38216  mblfinlem3  38545  ismblfin  38547  itg2addnc  38560  ftc1anc  38587  isbnd2  38685  isbnd3  38686  ssbnd  38690  ispridlc  38972  lshpkrlem6  40140  athgt  40481  3dim1  40492  3dim2  40493  lvolex3N  40563  llncvrlpln2  40582  lplncvrlvol2  40640  linepsubN  40777  lncvrelatN  40806  linepsubclN  40976  sn-negex12  43436  fidomncyc  43561  fsuppind  43580  eldioph2  43726  eldioph2b  43727  diophin  43736  diophun  43737  fphpdo  43777  irrapxlem3  43784  irrapxlem5  43786  pell1234qrne0  43813  pell1234qrreccl  43814  pell1234qrmulcl  43815  pell14qrgt0  43819  pell14qrdich  43829  pell1qrge1  43830  pell1qrgap  43834  pellqrex  43839  rmxycomplete  43877  jm2.27  43968  stoweidlem49  47003  m1modmmod  48378  ichreuopeq  48499  prproropf1olem2  48530  prproropf1olem4  48532  paireqne  48537  reupr  48548  nprmmul2  48554  nprmdvdsfacm1  48653  requad2  48665  gbowgt5  48804  isgrtri  48985  grimgrtri  48991  usgrgrtrirex  48992  gpgvtx0  49095  gpgvtx1  49096  gpgedgvtx0  49103  gpgedgvtx1  49104  pgn4cyclex  49168  prelrrx2b  49770