Theorem rexlimdvv 3217

Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 22-Jul-2004.)

Hypothesis

Ref	Expression
rexlimdvv.1	⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝜓 → 𝜒)))

Assertion

Ref	Expression
rexlimdvv	⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 → 𝜒))

Distinct variable groups:   𝑥,𝑦,𝜑   𝜒,𝑥,𝑦   𝑦,𝐴

Allowed substitution hints:   𝜓(𝑥,𝑦)   𝐴(𝑥)   𝐵(𝑥,𝑦)

Proof of Theorem rexlimdvv

Step	Hyp	Ref	Expression
1		rexlimdvv.1	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝜓 → 𝜒)))
2	1	expdimp 456	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ 𝐵 → (𝜓 → 𝜒)))
3	2	rexlimdv 3160	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∃𝑦 ∈ 𝐵 𝜓 → 𝜒))
4	3	rexlimdva 3162	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 → 𝜒))

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2141  ∃wrex 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-rex 3086

This theorem is referenced by:  rexlimdvva  3218  fprb  7174  f1oiso2  7332  omeu  8549  xpdom2  9040  rex2dom  9193  elfiun  9373  rankxplim3  9836  brdom6disj  10486  fpwwe2lem11  10596  tskxpss  10727  genpss  10959  genpcd  10961  genpnmax  10962  distrlem1pr  10980  distrlem5pr  10982  ltexprlem6  10996  reclem4pr  11005  supadd  12157  supmullem1  12159  supmullem2  12160  qaddcl  12963  qmulcl  12965  01sqrexlem6  15257  caubnd  15369  summo  15727  bezoutlem3  16558  bezoutlem4  16559  dvdsgcd  16561  gcddiv  16568  pceu  16865  pcqcl  16875  symgpssefmnd  19419  lspfixed  21178  lspexch  21179  lsmcv  21191  lspsolvlem  21192  hausnei2  23393  uncmp  23443  txcnp  23660  tx1stc  23690  fbasrn  23924  rnelfmlem  23992  blssps  24464  blss  24465  tgqioo  24840  ovolunlem2  25540  2sqnn  27480  madebdayim  27958  ax5seg  29085  axpasch  29088  axeuclid  29110  upgredg2vtx  29288  pjhthmo  31451  shmodsi  31538  pjpjpre  31568  chscllem4  31789  sumdmdlem  32567  cdj3lem2a  32585  cdj3lem2b  32586  cdj3lem3a  32588  dya2iocnrect  34539  satffunlem2lem1  35718  btwndiff  36341  btwnconn1lem13  36413  btwnconn1lem14  36414  brsegle  36422  segletr  36428  segleantisym  36429  nn0prpwlem  36646  ismblfin  38124  heibor1lem  38272  crngohomfo  38469  lsmsat  39596  3dim1  40055  3dim3  40057  1cvratex  40061  atcvrlln2  40107  atcvrlln  40108  lplnnlelln  40131  llncvrlpln2  40145  lplnexllnN  40152  2llnjN  40155  lvolnlelln  40172  lvolnlelpln  40173  lplncvrlvol2  40203  2lplnj  40208  lneq2at  40366  lnatexN  40367  lncvrat  40370  lncmp  40371  paddasslem15  40422  paddasslem16  40423  pmodlem2  40435  pmapjoin  40440  llnexchb2  40457  lhp2lt  40589  cdlemf  41151  cdlemg1cex  41176  cdlemg2ce  41180  cdlemn11pre  41798  dihord2pre  41813  dihord4  41846  dihmeetlem20N  41914  mapdpglem24  42292  mapdpglem32  42293  baerlem3lem2  42298  baerlem5alem2  42299  baerlem5blem2  42300  hdmapglem7  42517  sn-addlid  42977  rexlimdv3d  43228  mzpcompact2lem  43296  pellex  43376  onexomgt  43782  onexoegt  43785  oaun3lem1  43915  oaun3lem2  43916  disjrnmpt2  45730  mullimc  46156  mullimcf  46163  addlimc  46186  limclner  46189  fourierdlem42  46687  fourierdlem80  46724  fourierdlem97  46741  sge0resplit  46944  volicorescl  47091  opnvonmbllem2  47171  smfaddlem1  47301  smflimlem6  47314  gbepos  48344  gbowpos  48345  gbegt5  48347  gboge9  48350  isuspgrimlem  48481  usgrgrtrirex  48536  isubgr3stgrlem6  48557  gpgcubic  48665  gpg5nbgr3star  48667  pgnbgreunbgrlem3  48704  pgnbgreunbgrlem6  48710  pgnbgreunbgr  48711  seposep  49511  iscnrm3lem6  49523