Theorem rexlimdvv 3185

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ∃wrex 3053

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 207  df-an 396  df-ex 1780  df-rex 3054

This theorem is referenced by:  rexlimdvva  3186  fprb  7134  f1oiso2  7293  omeu  8510  xpdom2  8996  rex2dom  9152  elfiun  9339  rankxplim3  9796  brdom6disj  10445  fpwwe2lem11  10554  tskxpss  10685  genpss  10917  genpcd  10919  genpnmax  10920  distrlem1pr  10938  distrlem5pr  10940  ltexprlem6  10954  reclem4pr  10963  supadd  12111  supmullem1  12113  supmullem2  12114  qaddcl  12884  qmulcl  12886  01sqrexlem6  15172  caubnd  15284  summo  15642  bezoutlem3  16470  bezoutlem4  16471  dvdsgcd  16473  gcddiv  16480  pceu  16776  pcqcl  16786  symgpssefmnd  19293  lspfixed  21053  lspexch  21054  lsmcv  21066  lspsolvlem  21067  hausnei2  23256  uncmp  23306  txcnp  23523  tx1stc  23553  fbasrn  23787  rnelfmlem  23855  blssps  24328  blss  24329  tgqioo  24704  ovolunlem2  25415  2sqnn  27366  madebdayim  27820  ax5seg  28901  axpasch  28904  axeuclid  28926  upgredg2vtx  29104  pjhthmo  31264  shmodsi  31351  pjpjpre  31381  chscllem4  31602  sumdmdlem  32380  cdj3lem2a  32398  cdj3lem2b  32399  cdj3lem3a  32401  dya2iocnrect  34248  satffunlem2lem1  35376  btwndiff  36000  btwnconn1lem13  36072  btwnconn1lem14  36073  brsegle  36081  segletr  36087  segleantisym  36088  nn0prpwlem  36295  ismblfin  37640  heibor1lem  37788  crngohomfo  37985  lsmsat  38986  3dim1  39446  3dim3  39448  1cvratex  39452  atcvrlln2  39498  atcvrlln  39499  lplnnlelln  39522  llncvrlpln2  39536  lplnexllnN  39543  2llnjN  39546  lvolnlelln  39563  lvolnlelpln  39564  lplncvrlvol2  39594  2lplnj  39599  lneq2at  39757  lnatexN  39758  lncvrat  39761  lncmp  39762  paddasslem15  39813  paddasslem16  39814  pmodlem2  39826  pmapjoin  39831  llnexchb2  39848  lhp2lt  39980  cdlemf  40542  cdlemg1cex  40567  cdlemg2ce  40571  cdlemn11pre  41189  dihord2pre  41204  dihord4  41237  dihmeetlem20N  41305  mapdpglem24  41683  mapdpglem32  41684  baerlem3lem2  41689  baerlem5alem2  41690  baerlem5blem2  41691  hdmapglem7  41908  sn-addlid  42377  rexlimdv3d  42656  mzpcompact2lem  42724  pellex  42808  onexomgt  43214  onexoegt  43217  oaun3lem1  43347  oaun3lem2  43348  disjrnmpt2  45166  mullimc  45598  mullimcf  45605  addlimc  45630  limclner  45633  fourierdlem42  46131  fourierdlem80  46168  fourierdlem97  46185  sge0resplit  46388  volicorescl  46535  opnvonmbllem2  46615  smfaddlem1  46745  smflimlem6  46758  gbepos  47743  gbowpos  47744  gbegt5  47746  gboge9  47749  isuspgrimlem  47880  usgrgrtrirex  47935  isubgr3stgrlem6  47956  gpgcubic  48064  gpg5nbgr3star  48066  pgnbgreunbgrlem3  48103  pgnbgreunbgrlem6  48109  pgnbgreunbgr  48110  seposep  48911  iscnrm3lem6  48923