Theorem rexlimdvv 3192

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  ∃wrex 3060

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 3061

This theorem is referenced by:  rexlimdvva  3193  fprb  7140  f1oiso2  7298  omeu  8512  xpdom2  9000  rex2dom  9153  elfiun  9333  rankxplim3  9793  brdom6disj  10442  fpwwe2lem11  10552  tskxpss  10683  genpss  10915  genpcd  10917  genpnmax  10918  distrlem1pr  10936  distrlem5pr  10938  ltexprlem6  10952  reclem4pr  10961  supadd  12110  supmullem1  12112  supmullem2  12113  qaddcl  12878  qmulcl  12880  01sqrexlem6  15170  caubnd  15282  summo  15640  bezoutlem3  16468  bezoutlem4  16469  dvdsgcd  16471  gcddiv  16478  pceu  16774  pcqcl  16784  symgpssefmnd  19325  lspfixed  21083  lspexch  21084  lsmcv  21096  lspsolvlem  21097  hausnei2  23297  uncmp  23347  txcnp  23564  tx1stc  23594  fbasrn  23828  rnelfmlem  23896  blssps  24368  blss  24369  tgqioo  24744  ovolunlem2  25455  2sqnn  27406  madebdayim  27884  ax5seg  29011  axpasch  29014  axeuclid  29036  upgredg2vtx  29214  pjhthmo  31377  shmodsi  31464  pjpjpre  31494  chscllem4  31715  sumdmdlem  32493  cdj3lem2a  32511  cdj3lem2b  32512  cdj3lem3a  32514  dya2iocnrect  34438  satffunlem2lem1  35598  btwndiff  36221  btwnconn1lem13  36293  btwnconn1lem14  36294  brsegle  36302  segletr  36308  segleantisym  36309  nn0prpwlem  36516  ismblfin  37858  heibor1lem  38006  crngohomfo  38203  lsmsat  39264  3dim1  39723  3dim3  39725  1cvratex  39729  atcvrlln2  39775  atcvrlln  39776  lplnnlelln  39799  llncvrlpln2  39813  lplnexllnN  39820  2llnjN  39823  lvolnlelln  39840  lvolnlelpln  39841  lplncvrlvol2  39871  2lplnj  39876  lneq2at  40034  lnatexN  40035  lncvrat  40038  lncmp  40039  paddasslem15  40090  paddasslem16  40091  pmodlem2  40103  pmapjoin  40108  llnexchb2  40125  lhp2lt  40257  cdlemf  40819  cdlemg1cex  40844  cdlemg2ce  40848  cdlemn11pre  41466  dihord2pre  41481  dihord4  41514  dihmeetlem20N  41582  mapdpglem24  41960  mapdpglem32  41961  baerlem3lem2  41966  baerlem5alem2  41967  baerlem5blem2  41968  hdmapglem7  42185  sn-addlid  42655  rexlimdv3d  42921  mzpcompact2lem  42989  pellex  43073  onexomgt  43479  onexoegt  43482  oaun3lem1  43612  oaun3lem2  43613  disjrnmpt2  45428  mullimc  45858  mullimcf  45865  addlimc  45888  limclner  45891  fourierdlem42  46389  fourierdlem80  46426  fourierdlem97  46443  sge0resplit  46646  volicorescl  46793  opnvonmbllem2  46873  smfaddlem1  47003  smflimlem6  47016  gbepos  48000  gbowpos  48001  gbegt5  48003  gboge9  48006  isuspgrimlem  48137  usgrgrtrirex  48192  isubgr3stgrlem6  48213  gpgcubic  48321  gpg5nbgr3star  48323  pgnbgreunbgrlem3  48360  pgnbgreunbgrlem6  48366  pgnbgreunbgr  48367  seposep  49167  iscnrm3lem6  49179