Theorem rexlimdvva 2676

Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 18-Jun-2014.)

Hypothesis

Ref	Expression
rexlimdvva.1	⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 → 𝜒))

Assertion

Ref	Expression
rexlimdvva	⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 → 𝜒))

Distinct variable groups:   𝑥,𝑦,𝜑   𝜒,𝑥,𝑦   𝑦,𝐴

Allowed substitution hints:   𝜓(𝑥,𝑦)   𝐴(𝑥)   𝐵(𝑥,𝑦)

Proof of Theorem rexlimdvva

Step	Hyp	Ref	Expression
1		rexlimdvva.1	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 → 𝜒))
2	1	ex 115	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝜓 → 𝜒)))
3	2	rexlimdvv 2675	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 → 𝜒))

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2209  ∃wrex 2529

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-i5r 1588

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533  df-rex 2534

This theorem is referenced by:  ovelrn  6231  f1o2ndf1  6457  eroveu  6893  eroprf  6895  genipv  7869  genpelvl  7872  genpelvu  7873  genprndl  7881  genprndu  7882  addlocpr  7896  addnqprlemrl  7917  addnqprlemru  7918  mulnqprlemrl  7933  mulnqprlemru  7934  ltsopr  7956  ltaddpr  7957  ltexprlemfl  7969  ltexprlemrl  7970  ltexprlemfu  7971  ltexprlemru  7972  cauappcvgprlemladdfu  8014  cauappcvgprlemladdfl  8015  caucvgprlemdisj  8034  caucvgprlemladdfu  8037  caucvgprprlemdisj  8062  apreap  8908  apreim  8924  apirr  8926  apsym  8927  apcotr  8928  apadd1  8929  apneg  8932  mulext1  8933  apti  8943  aprcl  8967  qapne  10021  qtri3or  10656  exbtwnzlemex  10665  rebtwn2z  10670  cjap  11653  rexanre  11967  climcn2  12056  summodc  12131  prodmodclem2  12325  prodmodc  12326  eirrap  12526  dvds2lem  12551  bezoutlemnewy  12754  bezoutlembi  12763  dvdsmulgcd  12783  divgcdcoprm0  12860  cncongr1  12862  sqrt2irrap  12939  pcqmul  13063  pcneg  13085  pcadd  13100  4sqlem1  13148  4sqlem2  13149  4sqlem4  13152  mul4sq  13154  4sqlem12  13162  4sqlem13m  13163  4sqlem18  13168  imasaddfnlemg  13615  imasmnd2  13739  imasgrp2  13893  imasrng  14233  imasring  14345  dvdsrtr  14384  isnzr2  14467  lss1d  14695  znidom  14967  restbasg  15195  txbas  15285  blin2  15459  xmettxlem  15536  xmettx  15537  addcncntoplem  15588  mulcncf  15635  plyf  15764  plyadd  15778  plymul  15779  plyco  15786  plycj  15788  plycn  15789  plyrecj  15790  dvply2g  15793  logbgcd1irr  15995  logbgcd1irrap  15998  2sqlem5  16155  2sqlem9  16160  upgrpredgv  16304  usgredg4  16373  usgr1vr  16406  qdiff  17006