Theorem rexlimdvva 3020

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

Syntax hints:   → wi 4   ∧ wa 383   ∈ wcel 1977  ∃wrex 2897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-ral 2901  df-rex 2902

This theorem is referenced by:  disjxiun  4579  disjxiunOLD  4580  f1prex  6439  f1o2ndf1  7172  uniinqs  7714  eroveu  7729  eroprf  7732  ralxpmap  7793  unxpdomlem3  8051  finsschain  8156  dffi3  8220  sornom  8982  genpv  9700  genpdm  9703  1re  9918  cnegex  10096  zaddcl  11294  rexanre  13934  o1lo1  14116  lo1resb  14143  o1resb  14145  rlimcn2  14169  climcn2  14171  o1of2  14191  o1rlimmul  14197  lo1add  14205  lo1mul  14206  summo  14295  o1fsum  14386  ntrivcvgmul  14473  prodmolem2  14504  prodmo  14505  dvds2lem  14832  bezoutlem4  15097  dvdsmulgcd  15112  divgcdcoprm0  15217  cncongr1  15219  pcqmul  15396  pcneg  15416  pcadd  15431  4sqlem1  15490  4sqlem2  15491  4sqlem4  15494  mul4sq  15496  4sqlem12  15498  4sqlem13  15499  4sqlem18  15504  vdwmc2  15521  vdwlem7  15529  vdwlem9  15531  vdwlem10  15532  vdwlem11  15533  ramlb  15561  ramub1lem2  15569  imasaddfnlem  16011  imasmnd2  17150  imasgrp2  17353  gaorber  17564  psgnunilem2  17738  psgneu  17749  lsmsubm  17891  lsmsubg  17892  lsmmod  17911  lsmdisj2  17918  pj1eu  17932  efgtlen  17962  efgredlem  17983  efgredeu  17988  efgcpbllemb  17991  frgpuptinv  18007  frgpup3lem  18013  qusabl  18091  frgpnabllem1  18099  frgpnabl  18101  cygabl  18115  dprdsubg  18246  ablfacrp  18288  pgpfac1lem3  18299  imasring  18442  dvdsrtr  18475  lss1d  18784  lsmcl  18904  lsmelval2  18906  lbsextlem2  18980  isnzr2  19084  qsssubdrg  19624  znfld  19728  cygznlem3  19737  psgnghm  19745  lsmcss  19855  mdetunilem7  20243  mdetunilem8  20244  cayleyhamilton0  20513  cayleyhamiltonALT  20515  restbas  20772  ordtbas2  20805  ordtbas  20806  cnhaus  20968  cldllycmp  21108  txbas  21180  ptbasin  21190  txcls  21217  xkoccn  21232  txindis  21247  txlly  21249  txnlly  21250  pthaus  21251  ptrescn  21252  txhaus  21260  tx1stc  21263  txkgen  21265  xkohaus  21266  xkoptsub  21267  xkopt  21268  xkoco1cn  21270  xkoco2cn  21271  xkoinjcn  21300  fmfnfmlem3  21570  fmfnfmlem4  21571  hausflimi  21594  hauspwpwf1  21601  txflf  21620  qustgplem  21734  blin2  22044  prdsxmslem2  22144  xrge0tsms  22445  addcnlem  22475  minveclem3b  23007  pmltpc  23026  evthicc2  23036  dyaddisj  23170  ismbfd  23213  mbfimaopnlem  23228  rolle  23557  dvcnvrelem1  23584  dvcvx  23587  itgsubst  23616  plyf  23758  plypf1  23772  plyadd  23777  plymul  23778  coeeu  23785  dgrlem  23789  coeid  23798  aalioulem6  23896  o1cxp  24501  dchrptlem2  24790  lgsdchr  24880  2sqlem5  24947  2sqlem9  24952  2sqb  24957  pntlemp  25099  pnt3  25101  ostthlem1  25116  ostth3  25127  axcontlem4  25647  axcontlem9  25652  sizeusglecusglem1  26012  el2wlksotot  26409  3cyclfrgra  26542  n4cyclfrgra  26545  frgrawopreg  26576  ubthlem3  27112  cdjreui  28675  cdj3i  28684  br8d  28802  xrofsup  28923  xrge0tsmsd  29116  qqhval2  29354  mbfmco2  29654  txpcon  30468  cvmlift2lem10  30548  cvmlift2lem12  30550  cvmlift3lem7  30561  cvmlift3lem8  30562  mclsppslem  30734  br8  30899  br6  30900  br4  30901  brsegle  31385  tailfb  31542  unbdqndv2  31672  mblfinlem3  32618  ismblfin  32620  itg2addnc  32634  ftc1anc  32663  isbnd2  32752  isbnd3  32753  ssbnd  32757  ispridlc  33039  lshpkrlem6  33420  athgt  33760  3dim1  33771  3dim2  33772  lvolex3N  33842  llncvrlpln2  33861  lplncvrlvol2  33919  linepsubN  34056  lncvrelatN  34085  linepsubclN  34255  eldioph2  36343  eldioph2b  36344  diophin  36354  diophun  36355  fphpdo  36399  irrapxlem3  36406  irrapxlem5  36408  pell1234qrne0  36435  pell1234qrreccl  36436  pell1234qrmulcl  36437  pell14qrgt0  36441  pell14qrdich  36451  pell1qrge1  36452  pell1qrgap  36456  pellqrex  36461  rmxycomplete  36500  jm2.27  36593  stoweidlem49  38942  gbogt5  40184  usgredg4  40444  nbuhgr2vtx1edgb  40574  wwlksnwwlksnon  41121  2pthon3v-av  41150  umgr3v3e3cycl  41351  3cyclfrgr  41458  n4cyclfrgr  41461  frgrwopreg  41486  m1modmmod  42110