Theorem rexlimdvv 3205

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2110  ∃wrex 3055

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-ral 3059  df-rex 3060

This theorem is referenced by:  rexlimdvva  3206  fprb  6998  f1oiso2  7150  omeu  8302  xpdom2  8729  elfiun  9035  rankxplim3  9480  brdom6disj  10129  fpwwe2lem11  10238  tskxpss  10369  genpss  10601  genpcd  10603  genpnmax  10604  distrlem1pr  10622  distrlem5pr  10624  ltexprlem6  10638  reclem4pr  10647  supadd  11783  supmullem1  11785  supmullem2  11786  qaddcl  12544  qmulcl  12546  sqrlem6  14794  caubnd  14905  summo  15264  bezoutlem3  16082  bezoutlem4  16083  dvdsgcd  16085  gcddiv  16092  pceu  16380  pcqcl  16390  symgpssefmnd  18760  lspfixed  20137  lspexch  20138  lsmcv  20150  lspsolvlem  20151  hausnei2  22222  uncmp  22272  txcnp  22489  tx1stc  22519  fbasrn  22753  rnelfmlem  22821  blssps  23294  blss  23295  tgqioo  23669  ovolunlem2  24367  2sqnn  26292  ax5seg  27001  axpasch  27004  axeuclid  27026  upgredg2vtx  27204  pjhthmo  29355  shmodsi  29442  pjpjpre  29472  chscllem4  29693  sumdmdlem  30471  cdj3lem2a  30489  cdj3lem2b  30490  cdj3lem3a  30492  dya2iocnrect  31932  satffunlem2lem1  33051  poxp3  33484  madebdayim  33764  btwndiff  34023  btwnconn1lem13  34095  btwnconn1lem14  34096  brsegle  34104  segletr  34110  segleantisym  34111  nn0prpwlem  34205  ismblfin  35512  heibor1lem  35661  crngohomfo  35858  lsmsat  36716  3dim1  37175  3dim3  37177  1cvratex  37181  atcvrlln2  37227  atcvrlln  37228  lplnnlelln  37251  llncvrlpln2  37265  lplnexllnN  37272  2llnjN  37275  lvolnlelln  37292  lvolnlelpln  37293  lplncvrlvol2  37323  2lplnj  37328  lneq2at  37486  lnatexN  37487  lncvrat  37490  lncmp  37491  paddasslem15  37542  paddasslem16  37543  pmodlem2  37555  pmapjoin  37560  llnexchb2  37577  lhp2lt  37709  cdlemf  38271  cdlemg1cex  38296  cdlemg2ce  38300  cdlemn11pre  38918  dihord2pre  38933  dihord4  38966  dihmeetlem20N  39034  mapdpglem24  39412  mapdpglem32  39413  baerlem3lem2  39418  baerlem5alem2  39419  baerlem5blem2  39420  hdmapglem7  39637  sn-addid2  40047  rexlimdv3d  40160  mzpcompact2lem  40228  pellex  40312  disjrnmpt2  42351  mullimc  42786  mullimcf  42793  addlimc  42818  limclner  42821  fourierdlem42  43319  fourierdlem80  43356  fourierdlem97  43373  sge0resplit  43573  volicorescl  43720  opnvonmbllem2  43800  smfaddlem1  43924  smflimlem6  43937  gbepos  44837  gbowpos  44838  gbegt5  44840  gboge9  44843  seposep  45846  iscnrm3lem6  45859