Theorem rexlimdvva 2668

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 2667	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 → 𝜒))

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2203  ∃wrex 2521

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-i5r 1584

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-ral 2525  df-rex 2526

This theorem is referenced by:  ovelrn  6202  f1o2ndf1  6423  eroveu  6859  eroprf  6861  genipv  7823  genpelvl  7826  genpelvu  7827  genprndl  7835  genprndu  7836  addlocpr  7850  addnqprlemrl  7871  addnqprlemru  7872  mulnqprlemrl  7887  mulnqprlemru  7888  ltsopr  7910  ltaddpr  7911  ltexprlemfl  7923  ltexprlemrl  7924  ltexprlemfu  7925  ltexprlemru  7926  cauappcvgprlemladdfu  7968  cauappcvgprlemladdfl  7969  caucvgprlemdisj  7988  caucvgprlemladdfu  7991  caucvgprprlemdisj  8016  apreap  8860  apreim  8876  apirr  8878  apsym  8879  apcotr  8880  apadd1  8881  apneg  8884  mulext1  8885  apti  8895  aprcl  8919  qapne  9970  qtri3or  10599  exbtwnzlemex  10608  rebtwn2z  10613  cjap  11587  rexanre  11901  climcn2  11990  summodc  12065  prodmodclem2  12259  prodmodc  12260  eirrap  12460  dvds2lem  12485  bezoutlemnewy  12688  bezoutlembi  12697  dvdsmulgcd  12717  divgcdcoprm0  12794  cncongr1  12796  sqrt2irrap  12873  pcqmul  12997  pcneg  13019  pcadd  13034  4sqlem1  13082  4sqlem2  13083  4sqlem4  13086  mul4sq  13088  4sqlem12  13096  4sqlem13m  13097  4sqlem18  13102  imasaddfnlemg  13519  imasmnd2  13657  imasgrp2  13819  imasrng  14092  imasring  14200  dvdsrtr  14238  isnzr2  14321  lss1d  14523  znidom  14797  restbasg  15025  txbas  15115  blin2  15289  xmettxlem  15366  xmettx  15367  addcncntoplem  15418  mulcncf  15465  plyf  15594  plyadd  15608  plymul  15609  plyco  15616  plycj  15618  plycn  15619  plyrecj  15620  dvply2g  15623  logbgcd1irr  15824  logbgcd1irrap  15827  2sqlem5  15984  2sqlem9  15989  upgrpredgv  16133  usgredg4  16202  usgr1vr  16235  qdiff  16825