Theorem rexlimdvv 3296

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

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2113  ∃wrex 3142

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 1910

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1780  df-ral 3146  df-rex 3147

This theorem is referenced by:  rexlimdvva  3297  fprb  6959  f1oiso2  7108  omeu  8214  xpdom2  8615  elfiun  8897  rankxplim3  9313  brdom6disj  9957  fpwwe2lem12  10066  tskxpss  10197  genpss  10429  genpcd  10431  genpnmax  10432  distrlem1pr  10450  distrlem5pr  10452  ltexprlem6  10466  reclem4pr  10475  supadd  11612  supmullem1  11614  supmullem2  11615  qaddcl  12367  qmulcl  12369  sqrlem6  14610  caubnd  14721  summo  15077  bezoutlem3  15892  bezoutlem4  15893  dvdsgcd  15895  gcddiv  15902  pceu  16186  pcqcl  16196  symgpssefmnd  18527  lspfixed  19903  lspexch  19904  lsmcv  19916  lspsolvlem  19917  hausnei2  21964  uncmp  22014  txcnp  22231  tx1stc  22261  fbasrn  22495  rnelfmlem  22563  blssps  23037  blss  23038  tgqioo  23411  ovolunlem2  24102  2sqnn  26018  ax5seg  26727  axpasch  26730  axeuclid  26752  upgredg2vtx  26929  pjhthmo  29082  shmodsi  29169  pjpjpre  29199  chscllem4  29420  sumdmdlem  30198  cdj3lem2a  30216  cdj3lem2b  30217  cdj3lem3a  30219  dya2iocnrect  31543  satffunlem2lem1  32655  btwndiff  33492  btwnconn1lem13  33564  btwnconn1lem14  33565  brsegle  33573  segletr  33579  segleantisym  33580  nn0prpwlem  33674  ismblfin  34937  heibor1lem  35091  crngohomfo  35288  lsmsat  36148  3dim1  36607  3dim3  36609  1cvratex  36613  atcvrlln2  36659  atcvrlln  36660  lplnnlelln  36683  llncvrlpln2  36697  lplnexllnN  36704  2llnjN  36707  lvolnlelln  36724  lvolnlelpln  36725  lplncvrlvol2  36755  2lplnj  36760  lneq2at  36918  lnatexN  36919  lncvrat  36922  lncmp  36923  paddasslem15  36974  paddasslem16  36975  pmodlem2  36987  pmapjoin  36992  llnexchb2  37009  lhp2lt  37141  cdlemf  37703  cdlemg1cex  37728  cdlemg2ce  37732  cdlemn11pre  38350  dihord2pre  38365  dihord4  38398  dihmeetlem20N  38466  mapdpglem24  38844  mapdpglem32  38845  baerlem3lem2  38850  baerlem5alem2  38851  baerlem5blem2  38852  hdmapglem7  39069  sn-addid2  39240  rexlimdv3d  39286  mzpcompact2lem  39354  pellex  39438  disjrnmpt2  41455  mullimc  41903  mullimcf  41910  addlimc  41935  limclner  41938  fourierdlem42  42441  fourierdlem80  42478  fourierdlem97  42495  sge0resplit  42695  volicorescl  42842  opnvonmbllem2  42922  smfaddlem1  43046  smflimlem6  43059  gbepos  43930  gbowpos  43931  gbegt5  43933  gboge9  43936