Theorem rexlimdvva 3212

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

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2107  ∃wrex 3071

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-rex 3072

This theorem is referenced by:  disjxiun  5146  reuop  6293  f1prex  7282  f1o2ndf1  8108  poxp2  8129  xpord2pred  8131  sexp2  8132  xpord3pred  8138  sexp3  8139  frrlem9  8279  uniinqs  8791  eroveu  8806  eroprf  8809  ralxpmap  8890  unxpdomlem3  9252  finsschain  9359  dffi3  9426  sornom  10272  genpv  10994  genpdm  10997  1re  11214  cnegex  11395  zaddcl  12602  rexanre  15293  o1lo1  15481  lo1resb  15508  o1resb  15510  rlimcn3  15534  climcn2  15537  o1of2  15557  o1rlimmul  15563  lo1add  15571  lo1mul  15572  summo  15663  o1fsum  15759  ntrivcvgmul  15848  prodmolem2  15879  prodmo  15880  dvds2lem  16212  bezoutlem4  16484  dvdsmulgcd  16497  divgcdcoprm0  16602  cncongr1  16604  pcqmul  16786  pcneg  16807  pcadd  16822  4sqlem1  16881  4sqlem2  16882  4sqlem4  16885  mul4sq  16887  4sqlem12  16889  4sqlem13  16890  4sqlem18  16895  vdwmc2  16912  vdwlem7  16920  vdwlem9  16922  vdwlem10  16923  vdwlem11  16924  ramlb  16952  ramub1lem2  16960  imasaddfnlem  17474  imasmnd2  18662  xpsmnd0  18666  imasgrp2  18938  cyccom  19080  gaorber  19172  psgnunilem2  19363  psgneu  19374  lsmsubm  19521  lsmsubg  19522  lsmmod  19543  lsmdisj2  19550  pj1eu  19564  efgtlen  19594  efgredlem  19615  efgredeu  19620  efgcpbllemb  19623  frgpuptinv  19639  frgpup3lem  19645  qusabl  19733  frgpnabllem1  19741  frgpnabl  19743  dprdsubg  19894  ablfacrp  19936  pgpfac1lem3  19947  imasring  20143  xpsring1d  20146  dvdsrtr  20182  isnzr2  20297  lss1d  20574  lsmcl  20694  lsmelval2  20696  lbsextlem2  20772  qsssubdrg  21004  znfld  21116  cygznlem3  21125  psgnghm  21133  lsmcss  21245  mdetunilem7  22120  mdetunilem8  22121  cayleyhamilton0  22391  cayleyhamiltonALT  22393  restbas  22662  ordtbas2  22695  ordtbas  22696  cnhaus  22858  cldllycmp  22999  txbas  23071  ptbasin  23081  txcls  23108  xkoccn  23123  txindis  23138  txlly  23140  txnlly  23141  pthaus  23142  ptrescn  23143  txhaus  23151  tx1stc  23154  txkgen  23156  xkohaus  23157  xkoptsub  23158  xkopt  23159  xkoco1cn  23161  xkoco2cn  23162  xkoinjcn  23191  fmfnfmlem3  23460  fmfnfmlem4  23461  hausflimi  23484  hauspwpwf1  23491  txflf  23510  qustgplem  23625  blin2  23935  prdsxmslem2  24038  xrge0tsms  24350  addcnlem  24380  minveclem3b  24945  pmltpc  24967  evthicc2  24977  dyaddisj  25113  ismbfd  25156  mbfimaopnlem  25172  rolle  25507  dvcnvrelem1  25534  dvcvx  25537  itgsubst  25566  plyf  25712  plypf1  25726  plyadd  25731  plymul  25732  coeeu  25739  dgrlem  25743  coeid  25752  aalioulem6  25850  logbgcd1irr  26299  o1cxp  26479  dchrptlem2  26768  lgsdchr  26858  2sqlem5  26925  2sqlem9  26930  2sqb  26935  2sqreulem1  26949  2sqreunnlem1  26952  2sqreunnltblem  26954  pntlemp  27113  pnt3  27115  ostthlem1  27130  ostth3  27141  nosupprefixmo  27203  noinfprefixmo  27204  addsproplem2  27454  negsproplem2  27503  mulsproplem9  27580  ssltmul1  27602  ssltmul2  27603  precsexlem8  27660  precsexlem9  27661  precsexlem10  27662  precsexlem11  27663  axcontlem4  28225  axcontlem9  28230  upgrpredgv  28399  edglnl  28403  numedglnl  28404  usgredg4  28474  nbuhgr2vtx1edgb  28609  2pthon3v  29197  umgr3v3e3cycl  29437  3cyclfrgr  29541  n4cyclfrgr  29544  frgrwopreg  29576  2clwwlk2clwwlk  29603  ubthlem3  30125  cdjreui  31685  cdj3i  31694  br8d  31839  xrofsup  31980  xrge0tsmsd  32209  qqhval2  32962  mbfmco2  33264  txpconn  34223  cvmlift2lem10  34303  cvmlift2lem12  34305  cvmlift3lem7  34316  cvmlift3lem8  34317  satfv0  34349  satfv0fun  34362  satffunlem2lem1  34395  mclsppslem  34574  br8  34726  br6  34727  br4  34728  brsegle  35080  tailfb  35262  unbdqndv2  35387  mblfinlem3  36527  ismblfin  36529  itg2addnc  36542  ftc1anc  36569  isbnd2  36651  isbnd3  36652  ssbnd  36656  ispridlc  36938  lshpkrlem6  37985  athgt  38327  3dim1  38338  3dim2  38339  lvolex3N  38409  llncvrlpln2  38428  lplncvrlvol2  38486  linepsubN  38623  lncvrelatN  38652  linepsubclN  38822  fsuppind  41162  sn-negex12  41289  flt4lem7  41401  nna4b4nsq  41402  eldioph2  41500  eldioph2b  41501  diophin  41510  diophun  41511  fphpdo  41555  irrapxlem3  41562  irrapxlem5  41564  pell1234qrne0  41591  pell1234qrreccl  41592  pell1234qrmulcl  41593  pell14qrgt0  41597  pell14qrdich  41607  pell1qrge1  41608  pell1qrgap  41612  pellqrex  41617  rmxycomplete  41656  jm2.27  41747  stoweidlem49  44765  ichreuopeq  46141  prproropf1olem2  46172  prproropf1olem4  46174  paireqne  46179  reupr  46190  requad2  46291  gbowgt5  46430  isomuspgrlem1  46495  isomuspgrlem2b  46497  isomuspgrlem2d  46499  imasrng  46678  m1modmmod  47207  prelrrx2b  47400