Theorem rexlimdvv 3194

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

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

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 3055

This theorem is referenced by:  rexlimdvva  3195  fprb  7171  f1oiso2  7330  omeu  8552  xpdom2  9041  rex2dom  9200  elfiun  9388  rankxplim3  9841  brdom6disj  10492  fpwwe2lem11  10601  tskxpss  10732  genpss  10964  genpcd  10966  genpnmax  10967  distrlem1pr  10985  distrlem5pr  10987  ltexprlem6  11001  reclem4pr  11010  supadd  12158  supmullem1  12160  supmullem2  12161  qaddcl  12931  qmulcl  12933  01sqrexlem6  15220  caubnd  15332  summo  15690  bezoutlem3  16518  bezoutlem4  16519  dvdsgcd  16521  gcddiv  16528  pceu  16824  pcqcl  16834  symgpssefmnd  19333  lspfixed  21045  lspexch  21046  lsmcv  21058  lspsolvlem  21059  hausnei2  23247  uncmp  23297  txcnp  23514  tx1stc  23544  fbasrn  23778  rnelfmlem  23846  blssps  24319  blss  24320  tgqioo  24695  ovolunlem2  25406  2sqnn  27357  madebdayim  27806  ax5seg  28872  axpasch  28875  axeuclid  28897  upgredg2vtx  29075  pjhthmo  31238  shmodsi  31325  pjpjpre  31355  chscllem4  31576  sumdmdlem  32354  cdj3lem2a  32372  cdj3lem2b  32373  cdj3lem3a  32375  dya2iocnrect  34279  satffunlem2lem1  35398  btwndiff  36022  btwnconn1lem13  36094  btwnconn1lem14  36095  brsegle  36103  segletr  36109  segleantisym  36110  nn0prpwlem  36317  ismblfin  37662  heibor1lem  37810  crngohomfo  38007  lsmsat  39008  3dim1  39468  3dim3  39470  1cvratex  39474  atcvrlln2  39520  atcvrlln  39521  lplnnlelln  39544  llncvrlpln2  39558  lplnexllnN  39565  2llnjN  39568  lvolnlelln  39585  lvolnlelpln  39586  lplncvrlvol2  39616  2lplnj  39621  lneq2at  39779  lnatexN  39780  lncvrat  39783  lncmp  39784  paddasslem15  39835  paddasslem16  39836  pmodlem2  39848  pmapjoin  39853  llnexchb2  39870  lhp2lt  40002  cdlemf  40564  cdlemg1cex  40589  cdlemg2ce  40593  cdlemn11pre  41211  dihord2pre  41226  dihord4  41259  dihmeetlem20N  41327  mapdpglem24  41705  mapdpglem32  41706  baerlem3lem2  41711  baerlem5alem2  41712  baerlem5blem2  41713  hdmapglem7  41930  sn-addlid  42399  rexlimdv3d  42678  mzpcompact2lem  42746  pellex  42830  onexomgt  43237  onexoegt  43240  oaun3lem1  43370  oaun3lem2  43371  disjrnmpt2  45189  mullimc  45621  mullimcf  45628  addlimc  45653  limclner  45656  fourierdlem42  46154  fourierdlem80  46191  fourierdlem97  46208  sge0resplit  46411  volicorescl  46558  opnvonmbllem2  46638  smfaddlem1  46768  smflimlem6  46781  gbepos  47763  gbowpos  47764  gbegt5  47766  gboge9  47769  isuspgrimlem  47899  usgrgrtrirex  47953  isubgr3stgrlem6  47974  gpgcubic  48074  gpg5nbgr3star  48076  pgnbgreunbgrlem3  48112  pgnbgreunbgrlem6  48118  pgnbgreunbgr  48119  seposep  48918  iscnrm3lem6  48930