Theorem rexlimdvv 3209

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2105  ∃wrex 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-rex 3068

This theorem is referenced by:  rexlimdvva  3210  fprb  7213  f1oiso2  7371  omeu  8621  xpdom2  9105  rex2dom  9279  elfiun  9467  rankxplim3  9918  brdom6disj  10569  fpwwe2lem11  10678  tskxpss  10809  genpss  11041  genpcd  11043  genpnmax  11044  distrlem1pr  11062  distrlem5pr  11064  ltexprlem6  11078  reclem4pr  11087  supadd  12233  supmullem1  12235  supmullem2  12236  qaddcl  13004  qmulcl  13006  01sqrexlem6  15282  caubnd  15393  summo  15749  bezoutlem3  16574  bezoutlem4  16575  dvdsgcd  16577  gcddiv  16584  pceu  16879  pcqcl  16889  symgpssefmnd  19427  lspfixed  21147  lspexch  21148  lsmcv  21160  lspsolvlem  21161  hausnei2  23376  uncmp  23426  txcnp  23643  tx1stc  23673  fbasrn  23907  rnelfmlem  23975  blssps  24449  blss  24450  tgqioo  24835  ovolunlem2  25546  2sqnn  27497  madebdayim  27940  ax5seg  28967  axpasch  28970  axeuclid  28992  upgredg2vtx  29172  pjhthmo  31330  shmodsi  31417  pjpjpre  31447  chscllem4  31668  sumdmdlem  32446  cdj3lem2a  32464  cdj3lem2b  32465  cdj3lem3a  32467  dya2iocnrect  34262  satffunlem2lem1  35388  btwndiff  36008  btwnconn1lem13  36080  btwnconn1lem14  36081  brsegle  36089  segletr  36095  segleantisym  36096  nn0prpwlem  36304  ismblfin  37647  heibor1lem  37795  crngohomfo  37992  lsmsat  38989  3dim1  39449  3dim3  39451  1cvratex  39455  atcvrlln2  39501  atcvrlln  39502  lplnnlelln  39525  llncvrlpln2  39539  lplnexllnN  39546  2llnjN  39549  lvolnlelln  39566  lvolnlelpln  39567  lplncvrlvol2  39597  2lplnj  39602  lneq2at  39760  lnatexN  39761  lncvrat  39764  lncmp  39765  paddasslem15  39816  paddasslem16  39817  pmodlem2  39829  pmapjoin  39834  llnexchb2  39851  lhp2lt  39983  cdlemf  40545  cdlemg1cex  40570  cdlemg2ce  40574  cdlemn11pre  41192  dihord2pre  41207  dihord4  41240  dihmeetlem20N  41308  mapdpglem24  41686  mapdpglem32  41687  baerlem3lem2  41692  baerlem5alem2  41693  baerlem5blem2  41694  hdmapglem7  41911  sn-addlid  42410  rexlimdv3d  42670  mzpcompact2lem  42738  pellex  42822  onexomgt  43229  onexoegt  43232  oaun3lem1  43363  oaun3lem2  43364  disjrnmpt2  45130  mullimc  45571  mullimcf  45578  addlimc  45603  limclner  45606  fourierdlem42  46104  fourierdlem80  46141  fourierdlem97  46158  sge0resplit  46361  volicorescl  46508  opnvonmbllem2  46588  smfaddlem1  46718  smflimlem6  46731  gbepos  47682  gbowpos  47683  gbegt5  47685  gboge9  47688  isuspgrimlem  47811  usgrgrtrirex  47852  isubgr3stgrlem6  47873  gpgcubic  47969  gpg5nbgr3star  47971  seposep  48721  iscnrm3lem6  48734