Theorem rexlimdvv 3222

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  ∃wrex 3065

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 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-ral 3069  df-rex 3070

This theorem is referenced by:  rexlimdvva  3223  fprb  7069  f1oiso2  7223  omeu  8416  xpdom2  8854  elfiun  9189  rankxplim3  9639  brdom6disj  10288  fpwwe2lem11  10397  tskxpss  10528  genpss  10760  genpcd  10762  genpnmax  10763  distrlem1pr  10781  distrlem5pr  10783  ltexprlem6  10797  reclem4pr  10806  supadd  11943  supmullem1  11945  supmullem2  11946  qaddcl  12705  qmulcl  12707  sqrlem6  14959  caubnd  15070  summo  15429  bezoutlem3  16249  bezoutlem4  16250  dvdsgcd  16252  gcddiv  16259  pceu  16547  pcqcl  16557  symgpssefmnd  19003  lspfixed  20390  lspexch  20391  lsmcv  20403  lspsolvlem  20404  hausnei2  22504  uncmp  22554  txcnp  22771  tx1stc  22801  fbasrn  23035  rnelfmlem  23103  blssps  23577  blss  23578  tgqioo  23963  ovolunlem2  24662  2sqnn  26587  ax5seg  27306  axpasch  27309  axeuclid  27331  upgredg2vtx  27511  pjhthmo  29664  shmodsi  29751  pjpjpre  29781  chscllem4  30002  sumdmdlem  30780  cdj3lem2a  30798  cdj3lem2b  30799  cdj3lem3a  30801  dya2iocnrect  32248  satffunlem2lem1  33366  poxp3  33796  madebdayim  34070  btwndiff  34329  btwnconn1lem13  34401  btwnconn1lem14  34402  brsegle  34410  segletr  34416  segleantisym  34417  nn0prpwlem  34511  ismblfin  35818  heibor1lem  35967  crngohomfo  36164  lsmsat  37022  3dim1  37481  3dim3  37483  1cvratex  37487  atcvrlln2  37533  atcvrlln  37534  lplnnlelln  37557  llncvrlpln2  37571  lplnexllnN  37578  2llnjN  37581  lvolnlelln  37598  lvolnlelpln  37599  lplncvrlvol2  37629  2lplnj  37634  lneq2at  37792  lnatexN  37793  lncvrat  37796  lncmp  37797  paddasslem15  37848  paddasslem16  37849  pmodlem2  37861  pmapjoin  37866  llnexchb2  37883  lhp2lt  38015  cdlemf  38577  cdlemg1cex  38602  cdlemg2ce  38606  cdlemn11pre  39224  dihord2pre  39239  dihord4  39272  dihmeetlem20N  39340  mapdpglem24  39718  mapdpglem32  39719  baerlem3lem2  39724  baerlem5alem2  39725  baerlem5blem2  39726  hdmapglem7  39943  sn-addid2  40387  rexlimdv3d  40505  mzpcompact2lem  40573  pellex  40657  disjrnmpt2  42726  mullimc  43157  mullimcf  43164  addlimc  43189  limclner  43192  fourierdlem42  43690  fourierdlem80  43727  fourierdlem97  43744  sge0resplit  43944  volicorescl  44091  opnvonmbllem2  44171  smfaddlem1  44298  smflimlem6  44311  gbepos  45210  gbowpos  45211  gbegt5  45213  gboge9  45216  seposep  46219  iscnrm3lem6  46232