Theorem rexlimdvva 3221

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

Syntax hints:   → wi 4   ∧ wa 386   ∈ wcel 2107  ∃wrex 3091

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1824  df-ral 3095  df-rex 3096

This theorem is referenced by:  disjxiun  4883  f1prex  6811  f1o2ndf1  7566  uniinqs  8110  eroveu  8126  eroprf  8129  ralxpmap  8193  unxpdomlem3  8454  finsschain  8561  dffi3  8625  sornom  9434  genpv  10156  genpdm  10159  1re  10376  cnegex  10557  zaddcl  11769  rexanre  14493  o1lo1  14676  lo1resb  14703  o1resb  14705  rlimcn2  14729  climcn2  14731  o1of2  14751  o1rlimmul  14757  lo1add  14765  lo1mul  14766  summo  14855  o1fsum  14949  ntrivcvgmul  15037  prodmolem2  15068  prodmo  15069  dvds2lem  15401  bezoutlem4  15665  dvdsmulgcd  15680  divgcdcoprm0  15784  cncongr1  15786  pcqmul  15962  pcneg  15982  pcadd  15997  4sqlem1  16056  4sqlem2  16057  4sqlem4  16060  mul4sq  16062  4sqlem12  16064  4sqlem13  16065  4sqlem18  16070  vdwmc2  16087  vdwlem7  16095  vdwlem9  16097  vdwlem10  16098  vdwlem11  16099  ramlb  16127  ramub1lem2  16135  imasaddfnlem  16574  imasmnd2  17713  imasgrp2  17917  gaorber  18124  psgnunilem2  18299  psgneu  18310  lsmsubm  18452  lsmsubg  18453  lsmmod  18472  lsmdisj2  18479  pj1eu  18493  efgtlen  18523  efgredlem  18545  efgredlemOLD  18546  efgredeu  18551  efgcpbllemb  18554  frgpuptinv  18570  frgpup3lem  18576  qusabl  18654  frgpnabllem1  18662  frgpnabl  18664  cygabl  18678  dprdsubg  18810  ablfacrp  18852  pgpfac1lem3  18863  imasring  19006  dvdsrtr  19039  lss1d  19358  lsmcl  19478  lsmelval2  19480  lbsextlem2  19556  isnzr2  19660  qsssubdrg  20201  znfld  20304  cygznlem3  20313  psgnghm  20321  lsmcss  20435  mdetunilem7  20829  mdetunilem8  20830  cayleyhamilton0  21101  cayleyhamiltonALT  21103  restbas  21370  ordtbas2  21403  ordtbas  21404  cnhaus  21566  cldllycmp  21707  txbas  21779  ptbasin  21789  txcls  21816  xkoccn  21831  txindis  21846  txlly  21848  txnlly  21849  pthaus  21850  ptrescn  21851  txhaus  21859  tx1stc  21862  txkgen  21864  xkohaus  21865  xkoptsub  21866  xkopt  21867  xkoco1cn  21869  xkoco2cn  21870  xkoinjcn  21899  fmfnfmlem3  22168  fmfnfmlem4  22169  hausflimi  22192  hauspwpwf1  22199  txflf  22218  qustgplem  22332  blin2  22642  prdsxmslem2  22742  xrge0tsms  23045  addcnlem  23075  minveclem3b  23634  pmltpc  23654  evthicc2  23664  dyaddisj  23800  ismbfd  23843  mbfimaopnlem  23859  rolle  24190  dvcnvrelem1  24217  dvcvx  24220  itgsubst  24249  plyf  24391  plypf1  24405  plyadd  24410  plymul  24411  coeeu  24418  dgrlem  24422  coeid  24431  aalioulem6  24529  logbgcd1irr  24972  o1cxp  25153  dchrptlem2  25442  lgsdchr  25532  2sqlem5  25599  2sqlem9  25604  2sqb  25609  pntlemp  25751  pnt3  25753  ostthlem1  25768  ostth3  25779  axcontlem4  26316  axcontlem9  26321  upgrpredgv  26488  edglnl  26492  numedglnl  26493  usgredg4  26563  nbuhgr2vtx1edgb  26699  2pthon3v  27323  umgr3v3e3cycl  27587  3cyclfrgr  27696  n4cyclfrgr  27699  frgrwopreg  27731  2clwwlk2clwwlk  27761  2clwwlk2clwwlkOLD  27762  ubthlem3  28300  cdjreui  29863  cdj3i  29872  br8d  29985  xrofsup  30098  xrge0tsmsd  30347  qqhval2  30624  mbfmco2  30925  txpconn  31813  cvmlift2lem10  31893  cvmlift2lem12  31895  cvmlift3lem7  31906  cvmlift3lem8  31907  mclsppslem  32079  br8  32240  br6  32241  br4  32242  noprefixmo  32437  brsegle  32804  tailfb  32960  unbdqndv2  33084  mblfinlem3  34074  ismblfin  34076  itg2addnc  34089  ftc1anc  34118  isbnd2  34206  isbnd3  34207  ssbnd  34211  ispridlc  34493  lshpkrlem6  35269  athgt  35610  3dim1  35621  3dim2  35622  lvolex3N  35692  llncvrlpln2  35711  lplncvrlvol2  35769  linepsubN  35906  lncvrelatN  35935  linepsubclN  36105  eldioph2  38285  eldioph2b  38286  diophin  38296  diophun  38297  fphpdo  38341  irrapxlem3  38348  irrapxlem5  38350  pell1234qrne0  38377  pell1234qrreccl  38378  pell1234qrmulcl  38379  pell14qrgt0  38383  pell14qrdich  38393  pell1qrge1  38394  pell1qrgap  38398  pellqrex  38403  rmxycomplete  38441  jm2.27  38534  stoweidlem49  41193  prproropf1olem2  42443  prproropf1olem4  42445  paireqne  42450  requad2  42561  gbowgt5  42675  isomuspgrlem1  42740  isomuspgrlem2b  42742  isomuspgrlem2d  42744  m1modmmod  43331  prelrrx2b  43450