Theorem rexlimdvv 3208

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

Syntax hints:   → wi 4   ∧ wa 394   ∈ wcel 2104  ∃wrex 3068

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

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-rex 3069

This theorem is referenced by:  rexlimdvva  3209  fprb  7196  f1oiso2  7351  omeu  8587  xpdom2  9069  rex2dom  9248  elfiun  9427  rankxplim3  9878  brdom6disj  10529  fpwwe2lem11  10638  tskxpss  10769  genpss  11001  genpcd  11003  genpnmax  11004  distrlem1pr  11022  distrlem5pr  11024  ltexprlem6  11038  reclem4pr  11047  supadd  12186  supmullem1  12188  supmullem2  12189  qaddcl  12953  qmulcl  12955  01sqrexlem6  15198  caubnd  15309  summo  15667  bezoutlem3  16487  bezoutlem4  16488  dvdsgcd  16490  gcddiv  16497  pceu  16783  pcqcl  16793  symgpssefmnd  19304  lspfixed  20886  lspexch  20887  lsmcv  20899  lspsolvlem  20900  hausnei2  23077  uncmp  23127  txcnp  23344  tx1stc  23374  fbasrn  23608  rnelfmlem  23676  blssps  24150  blss  24151  tgqioo  24536  ovolunlem2  25247  2sqnn  27178  madebdayim  27619  ax5seg  28463  axpasch  28466  axeuclid  28488  upgredg2vtx  28668  pjhthmo  30822  shmodsi  30909  pjpjpre  30939  chscllem4  31160  sumdmdlem  31938  cdj3lem2a  31956  cdj3lem2b  31957  cdj3lem3a  31959  dya2iocnrect  33578  satffunlem2lem1  34693  btwndiff  35303  btwnconn1lem13  35375  btwnconn1lem14  35376  brsegle  35384  segletr  35390  segleantisym  35391  nn0prpwlem  35510  ismblfin  36832  heibor1lem  36980  crngohomfo  37177  lsmsat  38181  3dim1  38641  3dim3  38643  1cvratex  38647  atcvrlln2  38693  atcvrlln  38694  lplnnlelln  38717  llncvrlpln2  38731  lplnexllnN  38738  2llnjN  38741  lvolnlelln  38758  lvolnlelpln  38759  lplncvrlvol2  38789  2lplnj  38794  lneq2at  38952  lnatexN  38953  lncvrat  38956  lncmp  38957  paddasslem15  39008  paddasslem16  39009  pmodlem2  39021  pmapjoin  39026  llnexchb2  39043  lhp2lt  39175  cdlemf  39737  cdlemg1cex  39762  cdlemg2ce  39766  cdlemn11pre  40384  dihord2pre  40399  dihord4  40432  dihmeetlem20N  40500  mapdpglem24  40878  mapdpglem32  40879  baerlem3lem2  40884  baerlem5alem2  40885  baerlem5blem2  40886  hdmapglem7  41103  sn-addlid  41579  rexlimdv3d  41723  mzpcompact2lem  41791  pellex  41875  onexomgt  42292  onexoegt  42295  oaun3lem1  42426  oaun3lem2  42427  disjrnmpt2  44185  mullimc  44630  mullimcf  44637  addlimc  44662  limclner  44665  fourierdlem42  45163  fourierdlem80  45200  fourierdlem97  45217  sge0resplit  45420  volicorescl  45567  opnvonmbllem2  45647  smfaddlem1  45777  smflimlem6  45790  gbepos  46724  gbowpos  46725  gbegt5  46727  gboge9  46730  seposep  47645  iscnrm3lem6  47658