Theorem rexlimdvv 3194

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

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

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 3063

This theorem is referenced by:  rexlimdvva  3195  fprb  7150  f1oiso2  7308  omeu  8522  xpdom2  9012  rex2dom  9165  elfiun  9345  rankxplim3  9805  brdom6disj  10454  fpwwe2lem11  10564  tskxpss  10695  genpss  10927  genpcd  10929  genpnmax  10930  distrlem1pr  10948  distrlem5pr  10950  ltexprlem6  10964  reclem4pr  10973  supadd  12122  supmullem1  12124  supmullem2  12125  qaddcl  12890  qmulcl  12892  01sqrexlem6  15182  caubnd  15294  summo  15652  bezoutlem3  16480  bezoutlem4  16481  dvdsgcd  16483  gcddiv  16490  pceu  16786  pcqcl  16796  symgpssefmnd  19337  lspfixed  21095  lspexch  21096  lsmcv  21108  lspsolvlem  21109  hausnei2  23309  uncmp  23359  txcnp  23576  tx1stc  23606  fbasrn  23840  rnelfmlem  23908  blssps  24380  blss  24381  tgqioo  24756  ovolunlem2  25467  2sqnn  27418  madebdayim  27896  ax5seg  29023  axpasch  29026  axeuclid  29048  upgredg2vtx  29226  pjhthmo  31389  shmodsi  31476  pjpjpre  31506  chscllem4  31727  sumdmdlem  32505  cdj3lem2a  32523  cdj3lem2b  32524  cdj3lem3a  32526  dya2iocnrect  34458  satffunlem2lem1  35617  btwndiff  36240  btwnconn1lem13  36312  btwnconn1lem14  36313  brsegle  36321  segletr  36327  segleantisym  36328  nn0prpwlem  36535  ismblfin  37906  heibor1lem  38054  crngohomfo  38251  lsmsat  39378  3dim1  39837  3dim3  39839  1cvratex  39843  atcvrlln2  39889  atcvrlln  39890  lplnnlelln  39913  llncvrlpln2  39927  lplnexllnN  39934  2llnjN  39937  lvolnlelln  39954  lvolnlelpln  39955  lplncvrlvol2  39985  2lplnj  39990  lneq2at  40148  lnatexN  40149  lncvrat  40152  lncmp  40153  paddasslem15  40204  paddasslem16  40205  pmodlem2  40217  pmapjoin  40222  llnexchb2  40239  lhp2lt  40371  cdlemf  40933  cdlemg1cex  40958  cdlemg2ce  40962  cdlemn11pre  41580  dihord2pre  41595  dihord4  41628  dihmeetlem20N  41696  mapdpglem24  42074  mapdpglem32  42075  baerlem3lem2  42080  baerlem5alem2  42081  baerlem5blem2  42082  hdmapglem7  42299  sn-addlid  42768  rexlimdv3d  43034  mzpcompact2lem  43102  pellex  43186  onexomgt  43592  onexoegt  43595  oaun3lem1  43725  oaun3lem2  43726  disjrnmpt2  45541  mullimc  45970  mullimcf  45977  addlimc  46000  limclner  46003  fourierdlem42  46501  fourierdlem80  46538  fourierdlem97  46555  sge0resplit  46758  volicorescl  46905  opnvonmbllem2  46985  smfaddlem1  47115  smflimlem6  47128  gbepos  48112  gbowpos  48113  gbegt5  48115  gboge9  48118  isuspgrimlem  48249  usgrgrtrirex  48304  isubgr3stgrlem6  48325  gpgcubic  48433  gpg5nbgr3star  48435  pgnbgreunbgrlem3  48472  pgnbgreunbgrlem6  48478  pgnbgreunbgr  48479  seposep  49279  iscnrm3lem6  49291