Theorem rexlimdvva 3223

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  ∃wrex 3065

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 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-ral 3069  df-rex 3070

This theorem is referenced by:  disjxiun  5071  reuop  6196  f1prex  7156  f1o2ndf1  7963  frrlem9  8110  uniinqs  8586  eroveu  8601  eroprf  8604  ralxpmap  8684  unxpdomlem3  9029  finsschain  9126  dffi3  9190  sornom  10033  genpv  10755  genpdm  10758  1re  10975  cnegex  11156  zaddcl  12360  rexanre  15058  o1lo1  15246  lo1resb  15273  o1resb  15275  rlimcn3  15299  climcn2  15302  o1of2  15322  o1rlimmul  15328  lo1add  15336  lo1mul  15337  summo  15429  o1fsum  15525  ntrivcvgmul  15614  prodmolem2  15645  prodmo  15646  dvds2lem  15978  bezoutlem4  16250  dvdsmulgcd  16265  divgcdcoprm0  16370  cncongr1  16372  pcqmul  16554  pcneg  16575  pcadd  16590  4sqlem1  16649  4sqlem2  16650  4sqlem4  16653  mul4sq  16655  4sqlem12  16657  4sqlem13  16658  4sqlem18  16663  vdwmc2  16680  vdwlem7  16688  vdwlem9  16690  vdwlem10  16691  vdwlem11  16692  ramlb  16720  ramub1lem2  16728  imasaddfnlem  17239  imasmnd2  18422  imasgrp2  18690  cyccom  18822  gaorber  18914  psgnunilem2  19103  psgneu  19114  lsmsubm  19258  lsmsubg  19259  lsmmod  19281  lsmdisj2  19288  pj1eu  19302  efgtlen  19332  efgredlem  19353  efgredeu  19358  efgcpbllemb  19361  frgpuptinv  19377  frgpup3lem  19383  qusabl  19466  frgpnabllem1  19474  frgpnabl  19476  cygablOLD  19492  dprdsubg  19627  ablfacrp  19669  pgpfac1lem3  19680  imasring  19858  dvdsrtr  19894  lss1d  20225  lsmcl  20345  lsmelval2  20347  lbsextlem2  20421  isnzr2  20534  qsssubdrg  20657  znfld  20768  cygznlem3  20777  psgnghm  20785  lsmcss  20897  mdetunilem7  21767  mdetunilem8  21768  cayleyhamilton0  22038  cayleyhamiltonALT  22040  restbas  22309  ordtbas2  22342  ordtbas  22343  cnhaus  22505  cldllycmp  22646  txbas  22718  ptbasin  22728  txcls  22755  xkoccn  22770  txindis  22785  txlly  22787  txnlly  22788  pthaus  22789  ptrescn  22790  txhaus  22798  tx1stc  22801  txkgen  22803  xkohaus  22804  xkoptsub  22805  xkopt  22806  xkoco1cn  22808  xkoco2cn  22809  xkoinjcn  22838  fmfnfmlem3  23107  fmfnfmlem4  23108  hausflimi  23131  hauspwpwf1  23138  txflf  23157  qustgplem  23272  blin2  23582  prdsxmslem2  23685  xrge0tsms  23997  addcnlem  24027  minveclem3b  24592  pmltpc  24614  evthicc2  24624  dyaddisj  24760  ismbfd  24803  mbfimaopnlem  24819  rolle  25154  dvcnvrelem1  25181  dvcvx  25184  itgsubst  25213  plyf  25359  plypf1  25373  plyadd  25378  plymul  25379  coeeu  25386  dgrlem  25390  coeid  25399  aalioulem6  25497  logbgcd1irr  25944  o1cxp  26124  dchrptlem2  26413  lgsdchr  26503  2sqlem5  26570  2sqlem9  26575  2sqb  26580  2sqreulem1  26594  2sqreunnlem1  26597  2sqreunnltblem  26599  pntlemp  26758  pnt3  26760  ostthlem1  26775  ostth3  26786  axcontlem4  27335  axcontlem9  27340  upgrpredgv  27509  edglnl  27513  numedglnl  27514  usgredg4  27584  nbuhgr2vtx1edgb  27719  2pthon3v  28308  umgr3v3e3cycl  28548  3cyclfrgr  28652  n4cyclfrgr  28655  frgrwopreg  28687  2clwwlk2clwwlk  28714  ubthlem3  29234  cdjreui  30794  cdj3i  30803  br8d  30950  xrofsup  31090  xrge0tsmsd  31317  qqhval2  31932  mbfmco2  32232  txpconn  33194  cvmlift2lem10  33274  cvmlift2lem12  33276  cvmlift3lem7  33287  cvmlift3lem8  33288  satfv0  33320  satfv0fun  33333  satffunlem2lem1  33366  mclsppslem  33545  br8  33723  br6  33724  br4  33725  poxp2  33790  xpord2pred  33792  sexp2  33793  xpord3pred  33798  sexp3  33799  nosupprefixmo  33903  noinfprefixmo  33904  brsegle  34410  tailfb  34566  unbdqndv2  34691  mblfinlem3  35816  ismblfin  35818  itg2addnc  35831  ftc1anc  35858  isbnd2  35941  isbnd3  35942  ssbnd  35946  ispridlc  36228  lshpkrlem6  37129  athgt  37470  3dim1  37481  3dim2  37482  lvolex3N  37552  llncvrlpln2  37571  lplncvrlvol2  37629  linepsubN  37766  lncvrelatN  37795  linepsubclN  37965  fsuppind  40279  sn-negex12  40398  flt4lem7  40496  nna4b4nsq  40497  eldioph2  40584  eldioph2b  40585  diophin  40594  diophun  40595  fphpdo  40639  irrapxlem3  40646  irrapxlem5  40648  pell1234qrne0  40675  pell1234qrreccl  40676  pell1234qrmulcl  40677  pell14qrgt0  40681  pell14qrdich  40691  pell1qrge1  40692  pell1qrgap  40696  pellqrex  40701  rmxycomplete  40739  jm2.27  40830  stoweidlem49  43590  ichreuopeq  44925  prproropf1olem2  44956  prproropf1olem4  44958  paireqne  44963  reupr  44974  requad2  45075  gbowgt5  45214  isomuspgrlem1  45279  isomuspgrlem2b  45281  isomuspgrlem2d  45283  m1modmmod  45867  prelrrx2b  46060