Theorem rexlimdvv 3232

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

Syntax hints:   → wi 4   ∧ wa 387   ∈ wcel 2048  ∃wrex 3083

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-ral 3087  df-rex 3088

This theorem is referenced by:  rexlimdvva  3233  fprb  6777  f1oiso2  6922  omeu  8004  xpdom2  8400  elfiun  8681  rankxplim3  9096  brdom6disj  9744  fpwwe2lem12  9853  tskxpss  9984  genpss  10216  genpcd  10218  genpnmax  10219  distrlem1pr  10237  distrlem5pr  10239  ltexprlem6  10253  reclem4pr  10262  supadd  11402  supmullem1  11404  supmullem2  11405  qaddcl  12172  qmulcl  12174  sqrlem6  14458  caubnd  14569  summo  14924  bezoutlem3  15735  bezoutlem4  15736  dvdsgcd  15738  gcddiv  15745  pceu  16029  pcqcl  16039  lspfixed  19612  lspexch  19613  lsmcv  19625  lspsolvlem  19626  hausnei2  21655  uncmp  21705  txcnp  21922  tx1stc  21952  fbasrn  22186  rnelfmlem  22254  blssps  22727  blss  22728  tgqioo  23101  ovolunlem2  23792  2sqnn  25707  ax5seg  26417  axpasch  26420  axeuclid  26442  upgredg2vtx  26619  pjhthmo  28850  shmodsi  28937  pjpjpre  28967  chscllem4  29188  sumdmdlem  29966  cdj3lem2a  29984  cdj3lem2b  29985  cdj3lem3a  29987  dya2iocnrect  31141  btwndiff  32949  btwnconn1lem13  33021  btwnconn1lem14  33022  brsegle  33030  segletr  33036  segleantisym  33037  nn0prpwlem  33131  ismblfin  34322  heibor1lem  34477  crngohomfo  34674  lsmsat  35537  3dim1  35996  3dim3  35998  1cvratex  36002  atcvrlln2  36048  atcvrlln  36049  lplnnlelln  36072  llncvrlpln2  36086  lplnexllnN  36093  2llnjN  36096  lvolnlelln  36113  lvolnlelpln  36114  lplncvrlvol2  36144  2lplnj  36149  lneq2at  36307  lnatexN  36308  lncvrat  36311  lncmp  36312  paddasslem15  36363  paddasslem16  36364  pmodlem2  36376  pmapjoin  36381  llnexchb2  36398  lhp2lt  36530  cdlemf  37092  cdlemg1cex  37117  cdlemg2ce  37121  cdlemn11pre  37739  dihord2pre  37754  dihord4  37787  dihmeetlem20N  37855  mapdpglem24  38233  mapdpglem32  38234  baerlem3lem2  38239  baerlem5alem2  38240  baerlem5blem2  38241  hdmapglem7  38458  mzpcompact2lem  38688  pellex  38773  disjrnmpt2  40819  mullimc  41274  mullimcf  41281  addlimc  41306  limclner  41309  fourierdlem42  41811  fourierdlem80  41848  fourierdlem97  41865  sge0resplit  42065  volicorescl  42212  opnvonmbllem2  42292  smfaddlem1  42416  smflimlem6  42429  gbepos  43231  gbowpos  43232  gbegt5  43234  gboge9  43237