Theorem rexlimdvv 3295

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

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2114  ∃wrex 3141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-ral 3145  df-rex 3146

This theorem is referenced by:  rexlimdvva  3296  fprb  6958  f1oiso2  7107  omeu  8213  xpdom2  8614  elfiun  8896  rankxplim3  9312  brdom6disj  9956  fpwwe2lem12  10065  tskxpss  10196  genpss  10428  genpcd  10430  genpnmax  10431  distrlem1pr  10449  distrlem5pr  10451  ltexprlem6  10465  reclem4pr  10474  supadd  11611  supmullem1  11613  supmullem2  11614  qaddcl  12367  qmulcl  12369  sqrlem6  14609  caubnd  14720  summo  15076  bezoutlem3  15891  bezoutlem4  15892  dvdsgcd  15894  gcddiv  15901  pceu  16185  pcqcl  16195  symgpssefmnd  18526  lspfixed  19902  lspexch  19903  lsmcv  19915  lspsolvlem  19916  hausnei2  21963  uncmp  22013  txcnp  22230  tx1stc  22260  fbasrn  22494  rnelfmlem  22562  blssps  23036  blss  23037  tgqioo  23410  ovolunlem2  24101  2sqnn  26017  ax5seg  26726  axpasch  26729  axeuclid  26751  upgredg2vtx  26928  pjhthmo  29081  shmodsi  29168  pjpjpre  29198  chscllem4  29419  sumdmdlem  30197  cdj3lem2a  30215  cdj3lem2b  30216  cdj3lem3a  30218  dya2iocnrect  31541  satffunlem2lem1  32653  btwndiff  33490  btwnconn1lem13  33562  btwnconn1lem14  33563  brsegle  33571  segletr  33577  segleantisym  33578  nn0prpwlem  33672  ismblfin  34935  heibor1lem  35089  crngohomfo  35286  lsmsat  36146  3dim1  36605  3dim3  36607  1cvratex  36611  atcvrlln2  36657  atcvrlln  36658  lplnnlelln  36681  llncvrlpln2  36695  lplnexllnN  36702  2llnjN  36705  lvolnlelln  36722  lvolnlelpln  36723  lplncvrlvol2  36753  2lplnj  36758  lneq2at  36916  lnatexN  36917  lncvrat  36920  lncmp  36921  paddasslem15  36972  paddasslem16  36973  pmodlem2  36985  pmapjoin  36990  llnexchb2  37007  lhp2lt  37139  cdlemf  37701  cdlemg1cex  37726  cdlemg2ce  37730  cdlemn11pre  38348  dihord2pre  38363  dihord4  38396  dihmeetlem20N  38464  mapdpglem24  38842  mapdpglem32  38843  baerlem3lem2  38848  baerlem5alem2  38849  baerlem5blem2  38850  hdmapglem7  39067  sn-addid2  39241  rexlimdv3d  39287  mzpcompact2lem  39355  pellex  39439  disjrnmpt2  41456  mullimc  41904  mullimcf  41911  addlimc  41936  limclner  41939  fourierdlem42  42441  fourierdlem80  42478  fourierdlem97  42495  sge0resplit  42695  volicorescl  42842  opnvonmbllem2  42922  smfaddlem1  43046  smflimlem6  43059  gbepos  43930  gbowpos  43931  gbegt5  43933  gboge9  43936