Theorem rexlimdvva 2489

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

Syntax hints:   → wi 4   ∧ wa 102   ∈ wcel 1434  ∃wrex 2354

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441  ax-17 1460  ax-ial 1468  ax-i5r 1469

This theorem depends on definitions:  df-bi 115  df-nf 1391  df-ral 2358  df-rex 2359

This theorem is referenced by:  ovelrn  5700  f1o2ndf1  5900  eroveu  6284  eroprf  6286  genipv  6796  genpelvl  6799  genpelvu  6800  genprndl  6808  genprndu  6809  addlocpr  6823  addnqprlemrl  6844  addnqprlemru  6845  mulnqprlemrl  6860  mulnqprlemru  6861  ltsopr  6883  ltaddpr  6884  ltexprlemfl  6896  ltexprlemrl  6897  ltexprlemfu  6898  ltexprlemru  6899  cauappcvgprlemladdfu  6941  cauappcvgprlemladdfl  6942  caucvgprlemdisj  6961  caucvgprlemladdfu  6964  caucvgprprlemdisj  6989  apreap  7789  apreim  7805  apirr  7807  apsym  7808  apcotr  7809  apadd1  7810  apneg  7813  mulext1  7814  apti  7824  qapne  8840  qtri3or  9364  exbtwnzlemex  9371  rebtwn2z  9376  cjap  9977  rexanre  10290  climcn2  10332  dvds2lem  10398  bezoutlemnewy  10575  bezoutlembi  10584  dvdsmulgcd  10604  divgcdcoprm0  10673  cncongr1  10675  sqrt2irrap  10748