Theorem rexlimdvva 3201

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

Syntax hints:   → wi 4   ∧ wa 394   ∈ wcel 2098  ∃wrex 3059

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-rex 3060

This theorem is referenced by:  disjxiun  5146  reuop  6299  f1prex  7293  f1o2ndf1  8127  poxp2  8148  xpord2pred  8150  sexp2  8151  xpord3pred  8157  sexp3  8158  frrlem9  8300  uniinqs  8816  eroveu  8831  eroprf  8834  ralxpmap  8915  unxpdomlem3  9277  finsschain  9385  dffi3  9456  sornom  10302  genpv  11024  genpdm  11027  1re  11246  cnegex  11427  zaddcl  12635  rexanre  15329  o1lo1  15517  lo1resb  15544  o1resb  15546  rlimcn3  15570  climcn2  15573  o1of2  15593  o1rlimmul  15599  lo1add  15607  lo1mul  15608  summo  15699  o1fsum  15795  ntrivcvgmul  15884  prodmolem2  15915  prodmo  15916  dvds2lem  16249  bezoutlem4  16521  dvdsmulgcd  16534  divgcdcoprm0  16639  cncongr1  16641  pcqmul  16825  pcneg  16846  pcadd  16861  4sqlem1  16920  4sqlem2  16921  4sqlem4  16924  mul4sq  16926  4sqlem12  16928  4sqlem13  16929  4sqlem18  16934  vdwmc2  16951  vdwlem7  16959  vdwlem9  16961  vdwlem10  16962  vdwlem11  16963  ramlb  16991  ramub1lem2  16999  imasaddfnlem  17513  imasmnd2  18734  xpsmnd0  18738  imasgrp2  19019  cyccom  19166  gaorber  19271  psgnunilem2  19462  psgneu  19473  lsmsubm  19620  lsmsubg  19621  lsmmod  19642  lsmdisj2  19649  pj1eu  19663  efgtlen  19693  efgredlem  19714  efgredeu  19719  efgcpbllemb  19722  frgpuptinv  19738  frgpup3lem  19744  qusabl  19832  frgpnabllem1  19840  frgpnabl  19842  dprdsubg  19993  ablfacrp  20035  pgpfac1lem3  20046  imasrng  20129  imasring  20278  xpsring1d  20281  dvdsrtr  20319  isnzr2  20469  lss1d  20859  lsmcl  20980  lsmelval2  20982  lbsextlem2  21059  qsssubdrg  21376  znfld  21511  cygznlem3  21520  psgnghm  21529  lsmcss  21641  psdmul  22113  mdetunilem7  22564  mdetunilem8  22565  cayleyhamilton0  22835  cayleyhamiltonALT  22837  restbas  23106  ordtbas2  23139  ordtbas  23140  cnhaus  23302  cldllycmp  23443  txbas  23515  ptbasin  23525  txcls  23552  xkoccn  23567  txindis  23582  txlly  23584  txnlly  23585  pthaus  23586  ptrescn  23587  txhaus  23595  tx1stc  23598  txkgen  23600  xkohaus  23601  xkoptsub  23602  xkopt  23603  xkoco1cn  23605  xkoco2cn  23606  xkoinjcn  23635  fmfnfmlem3  23904  fmfnfmlem4  23905  hausflimi  23928  hauspwpwf1  23935  txflf  23954  qustgplem  24069  blin2  24379  prdsxmslem2  24482  xrge0tsms  24794  addcnlem  24824  minveclem3b  25400  pmltpc  25423  evthicc2  25433  dyaddisj  25569  ismbfd  25612  mbfimaopnlem  25628  rolle  25966  dvcnvrelem1  25994  dvcvx  25997  itgsubst  26028  plyf  26177  plypf1  26191  plyadd  26196  plymul  26197  coeeu  26204  dgrlem  26208  coeid  26217  aalioulem6  26317  logbgcd1irr  26771  o1cxp  26952  dchrptlem2  27243  lgsdchr  27333  2sqlem5  27400  2sqlem9  27405  2sqb  27410  2sqreulem1  27424  2sqreunnlem1  27427  2sqreunnltblem  27429  pntlemp  27588  pnt3  27590  ostthlem1  27605  ostth3  27616  nosupprefixmo  27679  noinfprefixmo  27680  addsproplem2  27933  negsproplem2  27987  mulsproplem9  28074  ssltmul1  28097  ssltmul2  28098  precsexlem8  28162  precsexlem9  28163  precsexlem10  28164  precsexlem11  28165  recut  28296  readdscl  28299  remulscl  28302  axcontlem4  28850  axcontlem9  28855  upgrpredgv  29024  edglnl  29028  numedglnl  29029  usgredg4  29102  nbuhgr2vtx1edgb  29237  2pthon3v  29826  umgr3v3e3cycl  30066  3cyclfrgr  30170  n4cyclfrgr  30173  frgrwopreg  30205  2clwwlk2clwwlk  30232  ubthlem3  30754  cdjreui  32314  cdj3i  32323  br8d  32479  xrofsup  32619  xrge0tsmsd  32861  qqhval2  33711  mbfmco2  34013  txpconn  34970  cvmlift2lem10  35050  cvmlift2lem12  35052  cvmlift3lem7  35063  cvmlift3lem8  35064  satfv0  35096  satfv0fun  35109  satffunlem2lem1  35142  mclsppslem  35321  br8  35478  br6  35479  br4  35480  brsegle  35832  tailfb  35989  unbdqndv2  36114  mblfinlem3  37260  ismblfin  37262  itg2addnc  37275  ftc1anc  37302  isbnd2  37384  isbnd3  37385  ssbnd  37389  ispridlc  37671  lshpkrlem6  38714  athgt  39056  3dim1  39067  3dim2  39068  lvolex3N  39138  llncvrlpln2  39157  lplncvrlvol2  39215  linepsubN  39352  lncvrelatN  39381  linepsubclN  39551  fsuppind  41955  sn-negex12  42103  flt4lem7  42215  nna4b4nsq  42216  eldioph2  42321  eldioph2b  42322  diophin  42331  diophun  42332  fphpdo  42376  irrapxlem3  42383  irrapxlem5  42385  pell1234qrne0  42412  pell1234qrreccl  42413  pell1234qrmulcl  42414  pell14qrgt0  42418  pell14qrdich  42428  pell1qrge1  42429  pell1qrgap  42433  pellqrex  42438  rmxycomplete  42477  jm2.27  42568  stoweidlem49  45572  ichreuopeq  46947  prproropf1olem2  46978  prproropf1olem4  46980  paireqne  46985  reupr  46996  requad2  47097  gbowgt5  47236  m1modmmod  47777  prelrrx2b  47970