Theorem rexlimdvv 3211

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

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2107  ∃wrex 3071

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-rex 3072

This theorem is referenced by:  rexlimdvva  3212  fprb  7195  f1oiso2  7349  omeu  8585  xpdom2  9067  rex2dom  9246  elfiun  9425  rankxplim3  9876  brdom6disj  10527  fpwwe2lem11  10636  tskxpss  10767  genpss  10999  genpcd  11001  genpnmax  11002  distrlem1pr  11020  distrlem5pr  11022  ltexprlem6  11036  reclem4pr  11045  supadd  12182  supmullem1  12184  supmullem2  12185  qaddcl  12949  qmulcl  12951  01sqrexlem6  15194  caubnd  15305  summo  15663  bezoutlem3  16483  bezoutlem4  16484  dvdsgcd  16486  gcddiv  16493  pceu  16779  pcqcl  16789  symgpssefmnd  19263  lspfixed  20741  lspexch  20742  lsmcv  20754  lspsolvlem  20755  hausnei2  22857  uncmp  22907  txcnp  23124  tx1stc  23154  fbasrn  23388  rnelfmlem  23456  blssps  23930  blss  23931  tgqioo  24316  ovolunlem2  25015  2sqnn  26942  madebdayim  27382  ax5seg  28196  axpasch  28199  axeuclid  28221  upgredg2vtx  28401  pjhthmo  30555  shmodsi  30642  pjpjpre  30672  chscllem4  30893  sumdmdlem  31671  cdj3lem2a  31689  cdj3lem2b  31690  cdj3lem3a  31692  dya2iocnrect  33280  satffunlem2lem1  34395  btwndiff  34999  btwnconn1lem13  35071  btwnconn1lem14  35072  brsegle  35080  segletr  35086  segleantisym  35087  nn0prpwlem  35207  ismblfin  36529  heibor1lem  36677  crngohomfo  36874  lsmsat  37878  3dim1  38338  3dim3  38340  1cvratex  38344  atcvrlln2  38390  atcvrlln  38391  lplnnlelln  38414  llncvrlpln2  38428  lplnexllnN  38435  2llnjN  38438  lvolnlelln  38455  lvolnlelpln  38456  lplncvrlvol2  38486  2lplnj  38491  lneq2at  38649  lnatexN  38650  lncvrat  38653  lncmp  38654  paddasslem15  38705  paddasslem16  38706  pmodlem2  38718  pmapjoin  38723  llnexchb2  38740  lhp2lt  38872  cdlemf  39434  cdlemg1cex  39459  cdlemg2ce  39463  cdlemn11pre  40081  dihord2pre  40096  dihord4  40129  dihmeetlem20N  40197  mapdpglem24  40575  mapdpglem32  40576  baerlem3lem2  40581  baerlem5alem2  40582  baerlem5blem2  40583  hdmapglem7  40800  sn-addlid  41277  rexlimdv3d  41421  mzpcompact2lem  41489  pellex  41573  onexomgt  41990  onexoegt  41993  oaun3lem1  42124  oaun3lem2  42125  disjrnmpt2  43886  mullimc  44332  mullimcf  44339  addlimc  44364  limclner  44367  fourierdlem42  44865  fourierdlem80  44902  fourierdlem97  44919  sge0resplit  45122  volicorescl  45269  opnvonmbllem2  45349  smfaddlem1  45479  smflimlem6  45492  gbepos  46426  gbowpos  46427  gbegt5  46429  gboge9  46432  seposep  47558  iscnrm3lem6  47571