Theorem rexlimdvva 2595

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 114	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝜓 → 𝜒)))
3	2	rexlimdvv 2594	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 → 𝜒))

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 2141  ∃wrex 2449

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-i5r 1528

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-ral 2453  df-rex 2454

This theorem is referenced by:  ovelrn  6001  f1o2ndf1  6207  eroveu  6604  eroprf  6606  genipv  7471  genpelvl  7474  genpelvu  7475  genprndl  7483  genprndu  7484  addlocpr  7498  addnqprlemrl  7519  addnqprlemru  7520  mulnqprlemrl  7535  mulnqprlemru  7536  ltsopr  7558  ltaddpr  7559  ltexprlemfl  7571  ltexprlemrl  7572  ltexprlemfu  7573  ltexprlemru  7574  cauappcvgprlemladdfu  7616  cauappcvgprlemladdfl  7617  caucvgprlemdisj  7636  caucvgprlemladdfu  7639  caucvgprprlemdisj  7664  apreap  8506  apreim  8522  apirr  8524  apsym  8525  apcotr  8526  apadd1  8527  apneg  8530  mulext1  8531  apti  8541  aprcl  8565  qapne  9598  qtri3or  10199  exbtwnzlemex  10206  rebtwn2z  10211  cjap  10870  rexanre  11184  climcn2  11272  summodc  11346  prodmodclem2  11540  prodmodc  11541  eirrap  11740  dvds2lem  11765  bezoutlemnewy  11951  bezoutlembi  11960  dvdsmulgcd  11980  divgcdcoprm0  12055  cncongr1  12057  sqrt2irrap  12134  pcqmul  12257  pcneg  12278  pcadd  12293  4sqlem1  12340  4sqlem2  12341  4sqlem4  12344  mul4sq  12346  restbasg  12962  txbas  13052  blin2  13226  xmettxlem  13303  xmettx  13304  addcncntoplem  13345  mulcncf  13385  logbgcd1irr  13679  logbgcd1irrap  13682  2sqlem5  13749  2sqlem9  13754