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  7134  f1oiso2  7292  omeu  8506  xpdom2  8991  rex2dom  9143  elfiun  9320  rankxplim3  9780  brdom6disj  10429  fpwwe2lem11  10538  tskxpss  10669  genpss  10901  genpcd  10903  genpnmax  10904  distrlem1pr  10922  distrlem5pr  10924  ltexprlem6  10938  reclem4pr  10947  supadd  12096  supmullem1  12098  supmullem2  12099  qaddcl  12869  qmulcl  12871  01sqrexlem6  15160  caubnd  15272  summo  15630  bezoutlem3  16458  bezoutlem4  16459  dvdsgcd  16461  gcddiv  16468  pceu  16764  pcqcl  16774  symgpssefmnd  19314  lspfixed  21071  lspexch  21072  lsmcv  21084  lspsolvlem  21085  hausnei2  23274  uncmp  23324  txcnp  23541  tx1stc  23571  fbasrn  23805  rnelfmlem  23873  blssps  24345  blss  24346  tgqioo  24721  ovolunlem2  25432  2sqnn  27383  madebdayim  27839  ax5seg  28923  axpasch  28926  axeuclid  28948  upgredg2vtx  29126  pjhthmo  31289  shmodsi  31376  pjpjpre  31406  chscllem4  31627  sumdmdlem  32405  cdj3lem2a  32423  cdj3lem2b  32424  cdj3lem3a  32426  dya2iocnrect  34301  satffunlem2lem1  35455  btwndiff  36078  btwnconn1lem13  36150  btwnconn1lem14  36151  brsegle  36159  segletr  36165  segleantisym  36166  nn0prpwlem  36373  ismblfin  37707  heibor1lem  37855  crngohomfo  38052  lsmsat  39113  3dim1  39572  3dim3  39574  1cvratex  39578  atcvrlln2  39624  atcvrlln  39625  lplnnlelln  39648  llncvrlpln2  39662  lplnexllnN  39669  2llnjN  39672  lvolnlelln  39689  lvolnlelpln  39690  lplncvrlvol2  39720  2lplnj  39725  lneq2at  39883  lnatexN  39884  lncvrat  39887  lncmp  39888  paddasslem15  39939  paddasslem16  39940  pmodlem2  39952  pmapjoin  39957  llnexchb2  39974  lhp2lt  40106  cdlemf  40668  cdlemg1cex  40693  cdlemg2ce  40697  cdlemn11pre  41315  dihord2pre  41330  dihord4  41363  dihmeetlem20N  41431  mapdpglem24  41809  mapdpglem32  41810  baerlem3lem2  41815  baerlem5alem2  41816  baerlem5blem2  41817  hdmapglem7  42034  sn-addlid  42503  rexlimdv3d  42781  mzpcompact2lem  42849  pellex  42933  onexomgt  43339  onexoegt  43342  oaun3lem1  43472  oaun3lem2  43473  disjrnmpt2  45290  mullimc  45721  mullimcf  45728  addlimc  45751  limclner  45754  fourierdlem42  46252  fourierdlem80  46289  fourierdlem97  46306  sge0resplit  46509  volicorescl  46656  opnvonmbllem2  46736  smfaddlem1  46866  smflimlem6  46879  gbepos  47863  gbowpos  47864  gbegt5  47866  gboge9  47869  isuspgrimlem  48000  usgrgrtrirex  48055  isubgr3stgrlem6  48076  gpgcubic  48184  gpg5nbgr3star  48186  pgnbgreunbgrlem3  48223  pgnbgreunbgrlem6  48229  pgnbgreunbgr  48230  seposep  49031  iscnrm3lem6  49043