Theorem rexlimdvv 3212

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ∃wrex 3070

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 3071

This theorem is referenced by:  rexlimdvva  3213  fprb  7214  f1oiso2  7372  omeu  8623  xpdom2  9107  rex2dom  9282  elfiun  9470  rankxplim3  9921  brdom6disj  10572  fpwwe2lem11  10681  tskxpss  10812  genpss  11044  genpcd  11046  genpnmax  11047  distrlem1pr  11065  distrlem5pr  11067  ltexprlem6  11081  reclem4pr  11090  supadd  12236  supmullem1  12238  supmullem2  12239  qaddcl  13007  qmulcl  13009  01sqrexlem6  15286  caubnd  15397  summo  15753  bezoutlem3  16578  bezoutlem4  16579  dvdsgcd  16581  gcddiv  16588  pceu  16884  pcqcl  16894  symgpssefmnd  19413  lspfixed  21130  lspexch  21131  lsmcv  21143  lspsolvlem  21144  hausnei2  23361  uncmp  23411  txcnp  23628  tx1stc  23658  fbasrn  23892  rnelfmlem  23960  blssps  24434  blss  24435  tgqioo  24821  ovolunlem2  25533  2sqnn  27483  madebdayim  27926  ax5seg  28953  axpasch  28956  axeuclid  28978  upgredg2vtx  29158  pjhthmo  31321  shmodsi  31408  pjpjpre  31438  chscllem4  31659  sumdmdlem  32437  cdj3lem2a  32455  cdj3lem2b  32456  cdj3lem3a  32458  dya2iocnrect  34283  satffunlem2lem1  35409  btwndiff  36028  btwnconn1lem13  36100  btwnconn1lem14  36101  brsegle  36109  segletr  36115  segleantisym  36116  nn0prpwlem  36323  ismblfin  37668  heibor1lem  37816  crngohomfo  38013  lsmsat  39009  3dim1  39469  3dim3  39471  1cvratex  39475  atcvrlln2  39521  atcvrlln  39522  lplnnlelln  39545  llncvrlpln2  39559  lplnexllnN  39566  2llnjN  39569  lvolnlelln  39586  lvolnlelpln  39587  lplncvrlvol2  39617  2lplnj  39622  lneq2at  39780  lnatexN  39781  lncvrat  39784  lncmp  39785  paddasslem15  39836  paddasslem16  39837  pmodlem2  39849  pmapjoin  39854  llnexchb2  39871  lhp2lt  40003  cdlemf  40565  cdlemg1cex  40590  cdlemg2ce  40594  cdlemn11pre  41212  dihord2pre  41227  dihord4  41260  dihmeetlem20N  41328  mapdpglem24  41706  mapdpglem32  41707  baerlem3lem2  41712  baerlem5alem2  41713  baerlem5blem2  41714  hdmapglem7  41931  sn-addlid  42434  rexlimdv3d  42694  mzpcompact2lem  42762  pellex  42846  onexomgt  43253  onexoegt  43256  oaun3lem1  43387  oaun3lem2  43388  disjrnmpt2  45193  mullimc  45631  mullimcf  45638  addlimc  45663  limclner  45666  fourierdlem42  46164  fourierdlem80  46201  fourierdlem97  46218  sge0resplit  46421  volicorescl  46568  opnvonmbllem2  46648  smfaddlem1  46778  smflimlem6  46791  gbepos  47745  gbowpos  47746  gbegt5  47748  gboge9  47751  isuspgrimlem  47874  usgrgrtrirex  47917  isubgr3stgrlem6  47938  gpgcubic  48035  gpg5nbgr3star  48037  seposep  48823  iscnrm3lem6  48835