Theorem rexlimdvv 3193

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 452	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ 𝐵 → (𝜓 → 𝜒)))
3	2	rexlimdv 3136	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∃𝑦 ∈ 𝐵 𝜓 → 𝜒))
4	3	rexlimdva 3138	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 → 𝜒))

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ∃wrex 3061

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 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-rex 3062

This theorem is referenced by:  rexlimdvva  3194  fprb  7149  f1oiso2  7307  omeu  8520  xpdom2  9010  rex2dom  9163  elfiun  9343  rankxplim3  9805  brdom6disj  10454  fpwwe2lem11  10564  tskxpss  10695  genpss  10927  genpcd  10929  genpnmax  10930  distrlem1pr  10948  distrlem5pr  10950  ltexprlem6  10964  reclem4pr  10973  supadd  12124  supmullem1  12126  supmullem2  12127  qaddcl  12915  qmulcl  12917  01sqrexlem6  15209  caubnd  15321  summo  15679  bezoutlem3  16510  bezoutlem4  16511  dvdsgcd  16513  gcddiv  16520  pceu  16817  pcqcl  16827  symgpssefmnd  19371  lspfixed  21126  lspexch  21127  lsmcv  21139  lspsolvlem  21140  hausnei2  23318  uncmp  23368  txcnp  23585  tx1stc  23615  fbasrn  23849  rnelfmlem  23917  blssps  24389  blss  24390  tgqioo  24765  ovolunlem2  25465  2sqnn  27402  madebdayim  27880  ax5seg  29007  axpasch  29010  axeuclid  29032  upgredg2vtx  29210  pjhthmo  31373  shmodsi  31460  pjpjpre  31490  chscllem4  31711  sumdmdlem  32489  cdj3lem2a  32507  cdj3lem2b  32508  cdj3lem3a  32510  dya2iocnrect  34425  satffunlem2lem1  35586  btwndiff  36209  btwnconn1lem13  36281  btwnconn1lem14  36282  brsegle  36290  segletr  36296  segleantisym  36297  nn0prpwlem  36504  ismblfin  37982  heibor1lem  38130  crngohomfo  38327  lsmsat  39454  3dim1  39913  3dim3  39915  1cvratex  39919  atcvrlln2  39965  atcvrlln  39966  lplnnlelln  39989  llncvrlpln2  40003  lplnexllnN  40010  2llnjN  40013  lvolnlelln  40030  lvolnlelpln  40031  lplncvrlvol2  40061  2lplnj  40066  lneq2at  40224  lnatexN  40225  lncvrat  40228  lncmp  40229  paddasslem15  40280  paddasslem16  40281  pmodlem2  40293  pmapjoin  40298  llnexchb2  40315  lhp2lt  40447  cdlemf  41009  cdlemg1cex  41034  cdlemg2ce  41038  cdlemn11pre  41656  dihord2pre  41671  dihord4  41704  dihmeetlem20N  41772  mapdpglem24  42150  mapdpglem32  42151  baerlem3lem2  42156  baerlem5alem2  42157  baerlem5blem2  42158  hdmapglem7  42375  sn-addlid  42836  rexlimdv3d  43115  mzpcompact2lem  43183  pellex  43263  onexomgt  43669  onexoegt  43672  oaun3lem1  43802  oaun3lem2  43803  disjrnmpt2  45618  mullimc  46046  mullimcf  46053  addlimc  46076  limclner  46079  fourierdlem42  46577  fourierdlem80  46614  fourierdlem97  46631  sge0resplit  46834  volicorescl  46981  opnvonmbllem2  47061  smfaddlem1  47191  smflimlem6  47204  gbepos  48234  gbowpos  48235  gbegt5  48237  gboge9  48240  isuspgrimlem  48371  usgrgrtrirex  48426  isubgr3stgrlem6  48447  gpgcubic  48555  gpg5nbgr3star  48557  pgnbgreunbgrlem3  48594  pgnbgreunbgrlem6  48600  pgnbgreunbgr  48601  seposep  49401  iscnrm3lem6  49413