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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ∃wrex 3064

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

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-ral 3068  df-rex 3069

This theorem is referenced by:  disjxiun  5067  reuop  6185  f1prex  7136  f1o2ndf1  7934  frrlem9  8081  uniinqs  8544  eroveu  8559  eroprf  8562  ralxpmap  8642  unxpdomlem3  8958  finsschain  9056  dffi3  9120  sornom  9964  genpv  10686  genpdm  10689  1re  10906  cnegex  11086  zaddcl  12290  rexanre  14986  o1lo1  15174  lo1resb  15201  o1resb  15203  rlimcn3  15227  climcn2  15230  o1of2  15250  o1rlimmul  15256  lo1add  15264  lo1mul  15265  summo  15357  o1fsum  15453  ntrivcvgmul  15542  prodmolem2  15573  prodmo  15574  dvds2lem  15906  bezoutlem4  16178  dvdsmulgcd  16193  divgcdcoprm0  16298  cncongr1  16300  pcqmul  16482  pcneg  16503  pcadd  16518  4sqlem1  16577  4sqlem2  16578  4sqlem4  16581  mul4sq  16583  4sqlem12  16585  4sqlem13  16586  4sqlem18  16591  vdwmc2  16608  vdwlem7  16616  vdwlem9  16618  vdwlem10  16619  vdwlem11  16620  ramlb  16648  ramub1lem2  16656  imasaddfnlem  17156  imasmnd2  18337  imasgrp2  18605  cyccom  18737  gaorber  18829  psgnunilem2  19018  psgneu  19029  lsmsubm  19173  lsmsubg  19174  lsmmod  19196  lsmdisj2  19203  pj1eu  19217  efgtlen  19247  efgredlem  19268  efgredeu  19273  efgcpbllemb  19276  frgpuptinv  19292  frgpup3lem  19298  qusabl  19381  frgpnabllem1  19389  frgpnabl  19391  cygablOLD  19407  dprdsubg  19542  ablfacrp  19584  pgpfac1lem3  19595  imasring  19773  dvdsrtr  19809  lss1d  20140  lsmcl  20260  lsmelval2  20262  lbsextlem2  20336  isnzr2  20447  qsssubdrg  20569  znfld  20680  cygznlem3  20689  psgnghm  20697  lsmcss  20809  mdetunilem7  21675  mdetunilem8  21676  cayleyhamilton0  21946  cayleyhamiltonALT  21948  restbas  22217  ordtbas2  22250  ordtbas  22251  cnhaus  22413  cldllycmp  22554  txbas  22626  ptbasin  22636  txcls  22663  xkoccn  22678  txindis  22693  txlly  22695  txnlly  22696  pthaus  22697  ptrescn  22698  txhaus  22706  tx1stc  22709  txkgen  22711  xkohaus  22712  xkoptsub  22713  xkopt  22714  xkoco1cn  22716  xkoco2cn  22717  xkoinjcn  22746  fmfnfmlem3  23015  fmfnfmlem4  23016  hausflimi  23039  hauspwpwf1  23046  txflf  23065  qustgplem  23180  blin2  23490  prdsxmslem2  23591  xrge0tsms  23903  addcnlem  23933  minveclem3b  24497  pmltpc  24519  evthicc2  24529  dyaddisj  24665  ismbfd  24708  mbfimaopnlem  24724  rolle  25059  dvcnvrelem1  25086  dvcvx  25089  itgsubst  25118  plyf  25264  plypf1  25278  plyadd  25283  plymul  25284  coeeu  25291  dgrlem  25295  coeid  25304  aalioulem6  25402  logbgcd1irr  25849  o1cxp  26029  dchrptlem2  26318  lgsdchr  26408  2sqlem5  26475  2sqlem9  26480  2sqb  26485  2sqreulem1  26499  2sqreunnlem1  26502  2sqreunnltblem  26504  pntlemp  26663  pnt3  26665  ostthlem1  26680  ostth3  26691  axcontlem4  27238  axcontlem9  27243  upgrpredgv  27412  edglnl  27416  numedglnl  27417  usgredg4  27487  nbuhgr2vtx1edgb  27622  2pthon3v  28209  umgr3v3e3cycl  28449  3cyclfrgr  28553  n4cyclfrgr  28556  frgrwopreg  28588  2clwwlk2clwwlk  28615  ubthlem3  29135  cdjreui  30695  cdj3i  30704  br8d  30851  xrofsup  30992  xrge0tsmsd  31219  qqhval2  31832  mbfmco2  32132  txpconn  33094  cvmlift2lem10  33174  cvmlift2lem12  33176  cvmlift3lem7  33187  cvmlift3lem8  33188  satfv0  33220  satfv0fun  33233  satffunlem2lem1  33266  mclsppslem  33445  br8  33629  br6  33630  br4  33631  poxp2  33717  xpord2pred  33719  sexp2  33720  xpord3pred  33725  sexp3  33726  nosupprefixmo  33830  noinfprefixmo  33831  brsegle  34337  tailfb  34493  unbdqndv2  34618  mblfinlem3  35743  ismblfin  35745  itg2addnc  35758  ftc1anc  35785  isbnd2  35868  isbnd3  35869  ssbnd  35873  ispridlc  36155  lshpkrlem6  37056  athgt  37397  3dim1  37408  3dim2  37409  lvolex3N  37479  llncvrlpln2  37498  lplncvrlvol2  37556  linepsubN  37693  lncvrelatN  37722  linepsubclN  37892  fsuppind  40202  sn-negex12  40319  flt4lem7  40412  nna4b4nsq  40413  eldioph2  40500  eldioph2b  40501  diophin  40510  diophun  40511  fphpdo  40555  irrapxlem3  40562  irrapxlem5  40564  pell1234qrne0  40591  pell1234qrreccl  40592  pell1234qrmulcl  40593  pell14qrgt0  40597  pell14qrdich  40607  pell1qrge1  40608  pell1qrgap  40612  pellqrex  40617  rmxycomplete  40655  jm2.27  40746  stoweidlem49  43480  ichreuopeq  44813  prproropf1olem2  44844  prproropf1olem4  44846  paireqne  44851  reupr  44862  requad2  44963  gbowgt5  45102  isomuspgrlem1  45167  isomuspgrlem2b  45169  isomuspgrlem2d  45171  m1modmmod  45755  prelrrx2b  45948