Theorem rexlimdvv 3019

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

Syntax hints:   → wi 4   ∧ wa 383   ∈ wcel 1977  ∃wrex 2897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-ral 2901  df-rex 2902

This theorem is referenced by:  rexlimdvva  3020  f1oiso2  6502  omeu  7552  xpdom2  7940  elfiun  8219  rankxplim3  8627  brdom6disj  9235  fpwwe2lem12  9342  tskxpss  9473  genpss  9705  genpcd  9707  genpnmax  9708  distrlem1pr  9726  distrlem5pr  9728  ltexprlem6  9742  reclem4pr  9751  supadd  10868  supmullem1  10870  supmullem2  10871  qaddcl  11680  qmulcl  11682  sqrlem6  13836  caubnd  13946  summo  14295  bezoutlem3  15096  bezoutlem4  15097  dvdsgcd  15099  gcddiv  15106  pceu  15389  pcqcl  15399  lspfixed  18949  lspexch  18950  lsmcv  18962  lspsolvlem  18963  hausnei2  20967  uncmp  21016  txcnp  21233  tx1stc  21263  fbasrn  21498  rnelfmlem  21566  blssps  22039  blss  22040  tgqioo  22411  ovolunlem2  23073  ax5seg  25618  axpasch  25621  axeuclid  25643  upgredg2vtx  25814  frgrawopreg  26576  pjhthmo  27545  shmodsi  27632  pjpjpre  27662  chscllem4  27883  sumdmdlem  28661  cdj3lem2a  28679  cdj3lem2b  28680  cdj3lem3a  28682  dya2iocnrect  29670  fprb  30916  btwndiff  31304  btwnconn1lem13  31376  btwnconn1lem14  31377  brsegle  31385  segletr  31391  segleantisym  31392  nn0prpwlem  31487  ismblfin  32620  heibor1lem  32778  crngohomfo  32975  lsmsat  33313  3dim1  33771  3dim3  33773  1cvratex  33777  atcvrlln2  33823  atcvrlln  33824  lplnnlelln  33847  llncvrlpln2  33861  lplnexllnN  33868  2llnjN  33871  lvolnlelln  33888  lvolnlelpln  33889  lplncvrlvol2  33919  2lplnj  33924  lneq2at  34082  lnatexN  34083  lncvrat  34086  lncmp  34087  paddasslem15  34138  paddasslem16  34139  pmodlem2  34151  pmapjoin  34156  llnexchb2  34173  lhp2lt  34305  cdlemf  34869  cdlemg1cex  34894  cdlemg2ce  34898  cdlemn11pre  35517  dihord2pre  35532  dihord4  35565  dihmeetlem20N  35633  mapdpglem24  36011  mapdpglem32  36012  baerlem3lem2  36017  baerlem5alem2  36018  baerlem5blem2  36019  hdmapglem7  36239  mzpcompact2lem  36332  pellex  36417  disjrnmpt2  38370  mullimc  38683  mullimcf  38690  addlimc  38715  limclner  38718  fourierdlem42  39042  fourierdlem80  39079  fourierdlem97  39096  sge0resplit  39299  volicorescl  39443  opnvonmbllem2  39523  smfaddlem1  39649  smflimlem6  39662  gbepos  40180  gbopos  40181  gbegt5  40183  gboage9  40186  frgrwopreg  41486