Theorem rexlimdvva 2484

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

Syntax hints:   → wi 4   ∧ wa 102   ∈ wcel 1433  ∃wrex 2349

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 1376  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-4 1440  ax-17 1459  ax-ial 1467  ax-i5r 1468

This theorem depends on definitions:  df-bi 115  df-nf 1390  df-ral 2353  df-rex 2354

This theorem is referenced by:  ovelrn  5669  f1o2ndf1  5869  eroveu  6220  eroprf  6222  genipv  6699  genpelvl  6702  genpelvu  6703  genprndl  6711  genprndu  6712  addlocpr  6726  addnqprlemrl  6747  addnqprlemru  6748  mulnqprlemrl  6763  mulnqprlemru  6764  ltsopr  6786  ltaddpr  6787  ltexprlemfl  6799  ltexprlemrl  6800  ltexprlemfu  6801  ltexprlemru  6802  cauappcvgprlemladdfu  6844  cauappcvgprlemladdfl  6845  caucvgprlemdisj  6864  caucvgprlemladdfu  6867  caucvgprprlemdisj  6892  apreap  7687  apreim  7703  apirr  7705  apsym  7706  apcotr  7707  apadd1  7708  apneg  7711  mulext1  7712  apti  7722  qapne  8724  qtri3or  9252  qbtwnzlemex  9259  rebtwn2z  9263  cjap  9793  rexanre  10106  climcn2  10148  dvds2lem  10207  bezoutlemnewy  10385  bezoutlembi  10394  dvdsmulgcd  10414  divgcdcoprm0  10483  cncongr1  10485  sqrt2irrap  10558