Theorem rexlimdvv 3221

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-ral 3068  df-rex 3069

This theorem is referenced by:  rexlimdvva  3222  fprb  7051  f1oiso2  7203  omeu  8378  xpdom2  8807  elfiun  9119  rankxplim3  9570  brdom6disj  10219  fpwwe2lem11  10328  tskxpss  10459  genpss  10691  genpcd  10693  genpnmax  10694  distrlem1pr  10712  distrlem5pr  10714  ltexprlem6  10728  reclem4pr  10737  supadd  11873  supmullem1  11875  supmullem2  11876  qaddcl  12634  qmulcl  12636  sqrlem6  14887  caubnd  14998  summo  15357  bezoutlem3  16177  bezoutlem4  16178  dvdsgcd  16180  gcddiv  16187  pceu  16475  pcqcl  16485  symgpssefmnd  18918  lspfixed  20305  lspexch  20306  lsmcv  20318  lspsolvlem  20319  hausnei2  22412  uncmp  22462  txcnp  22679  tx1stc  22709  fbasrn  22943  rnelfmlem  23011  blssps  23485  blss  23486  tgqioo  23869  ovolunlem2  24567  2sqnn  26492  ax5seg  27209  axpasch  27212  axeuclid  27234  upgredg2vtx  27414  pjhthmo  29565  shmodsi  29652  pjpjpre  29682  chscllem4  29903  sumdmdlem  30681  cdj3lem2a  30699  cdj3lem2b  30700  cdj3lem3a  30702  dya2iocnrect  32148  satffunlem2lem1  33266  poxp3  33723  madebdayim  33997  btwndiff  34256  btwnconn1lem13  34328  btwnconn1lem14  34329  brsegle  34337  segletr  34343  segleantisym  34344  nn0prpwlem  34438  ismblfin  35745  heibor1lem  35894  crngohomfo  36091  lsmsat  36949  3dim1  37408  3dim3  37410  1cvratex  37414  atcvrlln2  37460  atcvrlln  37461  lplnnlelln  37484  llncvrlpln2  37498  lplnexllnN  37505  2llnjN  37508  lvolnlelln  37525  lvolnlelpln  37526  lplncvrlvol2  37556  2lplnj  37561  lneq2at  37719  lnatexN  37720  lncvrat  37723  lncmp  37724  paddasslem15  37775  paddasslem16  37776  pmodlem2  37788  pmapjoin  37793  llnexchb2  37810  lhp2lt  37942  cdlemf  38504  cdlemg1cex  38529  cdlemg2ce  38533  cdlemn11pre  39151  dihord2pre  39166  dihord4  39199  dihmeetlem20N  39267  mapdpglem24  39645  mapdpglem32  39646  baerlem3lem2  39651  baerlem5alem2  39652  baerlem5blem2  39653  hdmapglem7  39870  sn-addid2  40308  rexlimdv3d  40421  mzpcompact2lem  40489  pellex  40573  disjrnmpt2  42615  mullimc  43047  mullimcf  43054  addlimc  43079  limclner  43082  fourierdlem42  43580  fourierdlem80  43617  fourierdlem97  43634  sge0resplit  43834  volicorescl  43981  opnvonmbllem2  44061  smfaddlem1  44185  smflimlem6  44198  gbepos  45098  gbowpos  45099  gbegt5  45101  gboge9  45104  seposep  46107  iscnrm3lem6  46120