Theorem rexlimdvva 3222

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2145  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-rex 3090

This theorem is referenced by:  rexlimdvvva  3223  disjxiun  5102  reuop  6284  f1prex  7272  f1o2ndf1  8105  poxp2  8127  xpord2pred  8129  sexp2  8130  xpord3pred  8136  sexp3  8137  frrlem9  8279  uniinqs  8783  eroveu  8798  eroprf  8801  ralxpmap  8882  unxpdomlem3  9206  finsschain  9304  dffi3  9379  sornom  10249  genpv  10972  genpdm  10975  1re  11196  cnegex  11379  zaddcl  12625  rexanre  15388  o1lo1  15578  lo1resb  15605  o1resb  15607  rlimcn3  15631  climcn2  15634  o1of2  15654  o1rlimmul  15660  lo1add  15668  lo1mul  15669  summo  15758  o1fsum  15855  ntrivcvgmul  15946  prodmolem2  15979  prodmo  15980  dvds2lem  16316  bezoutlem4  16590  dvdsmulgcd  16604  divgcdcoprm0  16713  cncongr1  16715  pcqmul  16903  pcneg  16924  pcadd  16939  4sqlem1  16998  4sqlem2  16999  4sqlem4  17002  mul4sq  17004  4sqlem12  17006  4sqlem13  17007  4sqlem18  17012  vdwmc2  17029  vdwlem7  17037  vdwlem9  17039  vdwlem10  17040  vdwlem11  17041  ramlb  17069  ramub1lem2  17077  imasaddfnlem  17572  imasmnd2  18822  xpsmnd0  18826  imasgrp2  19112  cyccom  19265  gaorber  19369  psgnunilem2  19556  psgneu  19567  lsmsubm  19714  lsmsubg  19715  lsmmod  19736  lsmdisj2  19743  pj1eu  19757  efgtlen  19787  efgredlem  19808  efgredeu  19813  efgcpbllemb  19816  frgpuptinv  19832  frgpup3lem  19838  qusabl  19926  frgpnabllem1  19934  frgpnabl  19936  dprdsubg  20087  ablfacrp  20129  pgpfac1lem3  20140  imasrng  20246  imasring  20403  xpsring1d  20406  dvdsrtr  20441  isnzr2  20592  lss1d  21053  lsmcl  21173  lsmelval2  21175  lbsextlem2  21252  qsssubdrg  21536  znfld  21670  cygznlem3  21679  psgnghm  21690  lsmcss  21802  psdmul  22289  mdetunilem7  22736  mdetunilem8  22737  cayleyhamilton0  23007  cayleyhamiltonALT  23009  restbas  23276  ordtbas2  23309  ordtbas  23310  cnhaus  23472  cldllycmp  23613  txbas  23685  ptbasin  23695  txcls  23722  xkoccn  23737  txindis  23752  txlly  23754  txnlly  23755  pthaus  23756  ptrescn  23757  txhaus  23765  tx1stc  23768  txkgen  23770  xkohaus  23771  xkoptsub  23772  xkopt  23773  xkoco1cn  23775  xkoco2cn  23776  xkoinjcn  23805  fmfnfmlem3  24074  fmfnfmlem4  24075  hausflimi  24098  hauspwpwf1  24105  txflf  24124  qustgplem  24239  blin2  24547  prdsxmslem2  24647  xrge0tsms  24953  addcnlem  24983  minveclem3b  25548  pmltpc  25570  evthicc2  25580  dyaddisj  25716  ismbfd  25759  mbfimaopnlem  25775  rolle  26110  dvcnvrelem1  26137  dvcvx  26140  itgsubst  26169  plyf  26316  plypf1  26330  plyadd  26335  plymul  26336  coeeu  26343  dgrlem  26347  coeid  26356  aalioulem6  26459  logbgcd1irr  26917  o1cxp  27097  dchrptlem2  27387  lgsdchr  27477  2sqlem5  27544  2sqlem9  27549  2sqb  27554  2sqreulem1  27568  2sqreunnlem1  27571  2sqreunnltblem  27573  pntlemp  27732  pnt3  27734  ostthlem1  27749  ostth3  27760  nosupprefixmo  27822  noinfprefixmo  27823  addsproplem2  28121  negsproplem2  28180  mulsproplem9  28275  sltmuls1  28298  sltmuls2  28299  precsexlem8  28365  precsexlem9  28366  precsexlem10  28367  precsexlem11  28368  onmulscl  28429  eucliddivs  28527  zaddscl  28545  zmulscld  28548  z12addscl  28628  z12sge0  28634  recut  28645  readdscl  28650  remulscl  28653  axcontlem4  29226  axcontlem9  29231  upgrpredgv  29398  edglnl  29402  numedglnl  29403  usgredg4  29476  nbuhgr2vtx1edgb  29611  2pthon3v  30201  umgr3v3e3cycl  30444  3cyclfrgr  30548  n4cyclfrgr  30551  frgrwopreg  30583  2clwwlk2clwwlk  30610  ubthlem3  31133  cdjreui  32693  cdj3i  32702  br8d  32865  xrofsup  33024  xrge0tsmsd  33306  qqhval2  34289  mbfmco2  34572  txpconn  35595  cvmlift2lem10  35675  cvmlift2lem12  35677  cvmlift3lem7  35688  cvmlift3lem8  35689  satfv0  35721  satfv0fun  35734  satffunlem2lem1  35767  mclsppslem  35946  br8  36119  br6  36120  br4  36121  brsegle  36471  tailfb  36750  unbdqndv2  36962  qdiff  37831  mblfinlem3  38170  ismblfin  38172  itg2addnc  38185  ftc1anc  38212  isbnd2  38294  isbnd3  38295  ssbnd  38299  ispridlc  38581  lshpkrlem6  39751  athgt  40092  3dim1  40103  3dim2  40104  lvolex3N  40174  llncvrlpln2  40193  lplncvrlvol2  40251  linepsubN  40388  lncvrelatN  40417  linepsubclN  40587  sn-negex12  43038  fidomncyc  43165  fsuppind  43184  flt4lem7  43253  nna4b4nsq  43254  eldioph2  43355  eldioph2b  43356  diophin  43365  diophun  43366  fphpdo  43406  irrapxlem3  43413  irrapxlem5  43415  pell1234qrne0  43442  pell1234qrreccl  43443  pell1234qrmulcl  43444  pell14qrgt0  43448  pell14qrdich  43458  pell1qrge1  43459  pell1qrgap  43463  pellqrex  43468  rmxycomplete  43506  jm2.27  43597  stoweidlem49  46621  m1modmmod  47956  ichreuopeq  48077  prproropf1olem2  48108  prproropf1olem4  48110  paireqne  48115  reupr  48126  nprmmul2  48132  nprmdvdsfacm1  48231  requad2  48243  gbowgt5  48382  isgrtri  48563  grimgrtri  48569  usgrgrtrirex  48570  gpgvtx0  48673  gpgvtx1  48674  gpgedgvtx0  48681  gpgedgvtx1  48682  pgn4cyclex  48746  prelrrx2b  49345