Theorem rexlimdvv 3196

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2119  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-rex 3065

This theorem is referenced by:  rexlimdvva  3197  fprb  7145  f1oiso2  7303  omeu  8517  xpdom2  9007  rex2dom  9160  elfiun  9340  rankxplim3  9803  brdom6disj  10452  fpwwe2lem11  10562  tskxpss  10693  genpss  10925  genpcd  10927  genpnmax  10928  distrlem1pr  10946  distrlem5pr  10948  ltexprlem6  10962  reclem4pr  10971  supadd  12122  supmullem1  12124  supmullem2  12125  qaddcl  12913  qmulcl  12915  01sqrexlem6  15207  caubnd  15319  summo  15677  bezoutlem3  16508  bezoutlem4  16509  dvdsgcd  16511  gcddiv  16518  pceu  16815  pcqcl  16825  symgpssefmnd  19369  lspfixed  21128  lspexch  21129  lsmcv  21141  lspsolvlem  21142  hausnei2  23343  uncmp  23393  txcnp  23610  tx1stc  23640  fbasrn  23874  rnelfmlem  23942  blssps  24414  blss  24415  tgqioo  24790  ovolunlem2  25490  2sqnn  27427  madebdayim  27905  ax5seg  29032  axpasch  29035  axeuclid  29057  upgredg2vtx  29235  pjhthmo  31398  shmodsi  31485  pjpjpre  31515  chscllem4  31736  sumdmdlem  32514  cdj3lem2a  32532  cdj3lem2b  32533  cdj3lem3a  32535  dya2iocnrect  34472  satffunlem2lem1  35639  btwndiff  36262  btwnconn1lem13  36334  btwnconn1lem14  36335  brsegle  36343  segletr  36349  segleantisym  36350  nn0prpwlem  36557  ismblfin  38035  heibor1lem  38183  crngohomfo  38380  lsmsat  39507  3dim1  39966  3dim3  39968  1cvratex  39972  atcvrlln2  40018  atcvrlln  40019  lplnnlelln  40042  llncvrlpln2  40056  lplnexllnN  40063  2llnjN  40066  lvolnlelln  40083  lvolnlelpln  40084  lplncvrlvol2  40114  2lplnj  40119  lneq2at  40277  lnatexN  40278  lncvrat  40281  lncmp  40282  paddasslem15  40333  paddasslem16  40334  pmodlem2  40346  pmapjoin  40351  llnexchb2  40368  lhp2lt  40500  cdlemf  41062  cdlemg1cex  41087  cdlemg2ce  41091  cdlemn11pre  41709  dihord2pre  41724  dihord4  41757  dihmeetlem20N  41825  mapdpglem24  42203  mapdpglem32  42204  baerlem3lem2  42209  baerlem5alem2  42210  baerlem5blem2  42211  hdmapglem7  42428  sn-addlid  42888  rexlimdv3d  43139  mzpcompact2lem  43207  pellex  43287  onexomgt  43693  onexoegt  43696  oaun3lem1  43826  oaun3lem2  43827  disjrnmpt2  45642  mullimc  46068  mullimcf  46075  addlimc  46098  limclner  46101  fourierdlem42  46599  fourierdlem80  46636  fourierdlem97  46653  sge0resplit  46856  volicorescl  47003  opnvonmbllem2  47083  smfaddlem1  47213  smflimlem6  47226  gbepos  48256  gbowpos  48257  gbegt5  48259  gboge9  48262  isuspgrimlem  48393  usgrgrtrirex  48448  isubgr3stgrlem6  48469  gpgcubic  48577  gpg5nbgr3star  48579  pgnbgreunbgrlem3  48616  pgnbgreunbgrlem6  48622  pgnbgreunbgr  48623  seposep  49423  iscnrm3lem6  49435