Theorem rexlimdvv 3188

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2111  ∃wrex 3056

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-rex 3057

This theorem is referenced by:  rexlimdvva  3189  fprb  7128  f1oiso2  7286  omeu  8500  xpdom2  8985  rex2dom  9137  elfiun  9314  rankxplim3  9771  brdom6disj  10420  fpwwe2lem11  10529  tskxpss  10660  genpss  10892  genpcd  10894  genpnmax  10895  distrlem1pr  10913  distrlem5pr  10915  ltexprlem6  10929  reclem4pr  10938  supadd  12087  supmullem1  12089  supmullem2  12090  qaddcl  12860  qmulcl  12862  01sqrexlem6  15151  caubnd  15263  summo  15621  bezoutlem3  16449  bezoutlem4  16450  dvdsgcd  16452  gcddiv  16459  pceu  16755  pcqcl  16765  symgpssefmnd  19306  lspfixed  21063  lspexch  21064  lsmcv  21076  lspsolvlem  21077  hausnei2  23266  uncmp  23316  txcnp  23533  tx1stc  23563  fbasrn  23797  rnelfmlem  23865  blssps  24337  blss  24338  tgqioo  24713  ovolunlem2  25424  2sqnn  27375  madebdayim  27831  ax5seg  28914  axpasch  28917  axeuclid  28939  upgredg2vtx  29117  pjhthmo  31277  shmodsi  31364  pjpjpre  31394  chscllem4  31615  sumdmdlem  32393  cdj3lem2a  32411  cdj3lem2b  32412  cdj3lem3a  32414  dya2iocnrect  34289  satffunlem2lem1  35436  btwndiff  36060  btwnconn1lem13  36132  btwnconn1lem14  36133  brsegle  36141  segletr  36147  segleantisym  36148  nn0prpwlem  36355  ismblfin  37700  heibor1lem  37848  crngohomfo  38045  lsmsat  39046  3dim1  39505  3dim3  39507  1cvratex  39511  atcvrlln2  39557  atcvrlln  39558  lplnnlelln  39581  llncvrlpln2  39595  lplnexllnN  39602  2llnjN  39605  lvolnlelln  39622  lvolnlelpln  39623  lplncvrlvol2  39653  2lplnj  39658  lneq2at  39816  lnatexN  39817  lncvrat  39820  lncmp  39821  paddasslem15  39872  paddasslem16  39873  pmodlem2  39885  pmapjoin  39890  llnexchb2  39907  lhp2lt  40039  cdlemf  40601  cdlemg1cex  40626  cdlemg2ce  40630  cdlemn11pre  41248  dihord2pre  41263  dihord4  41296  dihmeetlem20N  41364  mapdpglem24  41742  mapdpglem32  41743  baerlem3lem2  41748  baerlem5alem2  41749  baerlem5blem2  41750  hdmapglem7  41967  sn-addlid  42436  rexlimdv3d  42715  mzpcompact2lem  42783  pellex  42867  onexomgt  43273  onexoegt  43276  oaun3lem1  43406  oaun3lem2  43407  disjrnmpt2  45224  mullimc  45655  mullimcf  45662  addlimc  45685  limclner  45688  fourierdlem42  46186  fourierdlem80  46223  fourierdlem97  46240  sge0resplit  46443  volicorescl  46590  opnvonmbllem2  46670  smfaddlem1  46800  smflimlem6  46813  gbepos  47788  gbowpos  47789  gbegt5  47791  gboge9  47794  isuspgrimlem  47925  usgrgrtrirex  47980  isubgr3stgrlem6  48001  gpgcubic  48109  gpg5nbgr3star  48111  pgnbgreunbgrlem3  48148  pgnbgreunbgrlem6  48154  pgnbgreunbgr  48155  seposep  48956  iscnrm3lem6  48968