Theorem rexlimdvva 3202

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 3201	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 → 𝜒))

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913

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

This theorem is referenced by:  disjxiun  5094  reuop  6236  f1prex  7217  f1o2ndf1  8035  frrlem9  8185  uniinqs  8662  eroveu  8677  eroprf  8680  ralxpmap  8760  unxpdomlem3  9122  finsschain  9229  dffi3  9293  sornom  10139  genpv  10861  genpdm  10864  1re  11081  cnegex  11262  zaddcl  12466  rexanre  15158  o1lo1  15346  lo1resb  15373  o1resb  15375  rlimcn3  15399  climcn2  15402  o1of2  15422  o1rlimmul  15428  lo1add  15436  lo1mul  15437  summo  15529  o1fsum  15625  ntrivcvgmul  15714  prodmolem2  15745  prodmo  15746  dvds2lem  16078  bezoutlem4  16350  dvdsmulgcd  16363  divgcdcoprm0  16468  cncongr1  16470  pcqmul  16652  pcneg  16673  pcadd  16688  4sqlem1  16747  4sqlem2  16748  4sqlem4  16751  mul4sq  16753  4sqlem12  16755  4sqlem13  16756  4sqlem18  16761  vdwmc2  16778  vdwlem7  16786  vdwlem9  16788  vdwlem10  16789  vdwlem11  16790  ramlb  16818  ramub1lem2  16826  imasaddfnlem  17337  imasmnd2  18520  imasgrp2  18787  cyccom  18919  gaorber  19011  psgnunilem2  19200  psgneu  19211  lsmsubm  19355  lsmsubg  19356  lsmmod  19377  lsmdisj2  19384  pj1eu  19398  efgtlen  19428  efgredlem  19449  efgredeu  19454  efgcpbllemb  19457  frgpuptinv  19473  frgpup3lem  19479  qusabl  19562  frgpnabllem1  19570  frgpnabl  19572  dprdsubg  19722  ablfacrp  19764  pgpfac1lem3  19775  imasring  19953  dvdsrtr  19989  lss1d  20331  lsmcl  20451  lsmelval2  20453  lbsextlem2  20527  isnzr2  20640  qsssubdrg  20763  znfld  20874  cygznlem3  20883  psgnghm  20891  lsmcss  21003  mdetunilem7  21873  mdetunilem8  21874  cayleyhamilton0  22144  cayleyhamiltonALT  22146  restbas  22415  ordtbas2  22448  ordtbas  22449  cnhaus  22611  cldllycmp  22752  txbas  22824  ptbasin  22834  txcls  22861  xkoccn  22876  txindis  22891  txlly  22893  txnlly  22894  pthaus  22895  ptrescn  22896  txhaus  22904  tx1stc  22907  txkgen  22909  xkohaus  22910  xkoptsub  22911  xkopt  22912  xkoco1cn  22914  xkoco2cn  22915  xkoinjcn  22944  fmfnfmlem3  23213  fmfnfmlem4  23214  hausflimi  23237  hauspwpwf1  23244  txflf  23263  qustgplem  23378  blin2  23688  prdsxmslem2  23791  xrge0tsms  24103  addcnlem  24133  minveclem3b  24698  pmltpc  24720  evthicc2  24730  dyaddisj  24866  ismbfd  24909  mbfimaopnlem  24925  rolle  25260  dvcnvrelem1  25287  dvcvx  25290  itgsubst  25319  plyf  25465  plypf1  25479  plyadd  25484  plymul  25485  coeeu  25492  dgrlem  25496  coeid  25505  aalioulem6  25603  logbgcd1irr  26050  o1cxp  26230  dchrptlem2  26519  lgsdchr  26609  2sqlem5  26676  2sqlem9  26681  2sqb  26686  2sqreulem1  26700  2sqreunnlem1  26703  2sqreunnltblem  26705  pntlemp  26864  pnt3  26866  ostthlem1  26881  ostth3  26892  nosupprefixmo  26954  noinfprefixmo  26955  axcontlem4  27624  axcontlem9  27629  upgrpredgv  27798  edglnl  27802  numedglnl  27803  usgredg4  27873  nbuhgr2vtx1edgb  28008  2pthon3v  28596  umgr3v3e3cycl  28836  3cyclfrgr  28940  n4cyclfrgr  28943  frgrwopreg  28975  2clwwlk2clwwlk  29002  ubthlem3  29522  cdjreui  31082  cdj3i  31091  br8d  31235  xrofsup  31375  xrge0tsmsd  31602  qqhval2  32228  mbfmco2  32530  txpconn  33491  cvmlift2lem10  33571  cvmlift2lem12  33573  cvmlift3lem7  33584  cvmlift3lem8  33585  satfv0  33617  satfv0fun  33630  satffunlem2lem1  33663  mclsppslem  33842  br8  34012  br6  34013  br4  34014  poxp2  34072  xpord2pred  34074  sexp2  34075  xpord3pred  34080  sexp3  34081  addsproplem2  34234  brsegle  34547  tailfb  34703  unbdqndv2  34828  mblfinlem3  35970  ismblfin  35972  itg2addnc  35985  ftc1anc  36012  isbnd2  36095  isbnd3  36096  ssbnd  36100  ispridlc  36382  lshpkrlem6  37431  athgt  37773  3dim1  37784  3dim2  37785  lvolex3N  37855  llncvrlpln2  37874  lplncvrlvol2  37932  linepsubN  38069  lncvrelatN  38098  linepsubclN  38268  fsuppind  40588  sn-negex12  40707  flt4lem7  40807  nna4b4nsq  40808  eldioph2  40895  eldioph2b  40896  diophin  40905  diophun  40906  fphpdo  40950  irrapxlem3  40957  irrapxlem5  40959  pell1234qrne0  40986  pell1234qrreccl  40987  pell1234qrmulcl  40988  pell14qrgt0  40992  pell14qrdich  41002  pell1qrge1  41003  pell1qrgap  41007  pellqrex  41012  rmxycomplete  41051  jm2.27  41142  stoweidlem49  43976  ichreuopeq  45341  prproropf1olem2  45372  prproropf1olem4  45374  paireqne  45379  reupr  45390  requad2  45491  gbowgt5  45630  isomuspgrlem1  45695  isomuspgrlem2b  45697  isomuspgrlem2d  45699  m1modmmod  46283  prelrrx2b  46476