Theorem rexlimdvva 2591

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

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 2136  ∃wrex 2445

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 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522  ax-i5r 1523

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-ral 2449  df-rex 2450

This theorem is referenced by:  ovelrn  5990  f1o2ndf1  6196  eroveu  6592  eroprf  6594  genipv  7450  genpelvl  7453  genpelvu  7454  genprndl  7462  genprndu  7463  addlocpr  7477  addnqprlemrl  7498  addnqprlemru  7499  mulnqprlemrl  7514  mulnqprlemru  7515  ltsopr  7537  ltaddpr  7538  ltexprlemfl  7550  ltexprlemrl  7551  ltexprlemfu  7552  ltexprlemru  7553  cauappcvgprlemladdfu  7595  cauappcvgprlemladdfl  7596  caucvgprlemdisj  7615  caucvgprlemladdfu  7618  caucvgprprlemdisj  7643  apreap  8485  apreim  8501  apirr  8503  apsym  8504  apcotr  8505  apadd1  8506  apneg  8509  mulext1  8510  apti  8520  aprcl  8544  qapne  9577  qtri3or  10178  exbtwnzlemex  10185  rebtwn2z  10190  cjap  10848  rexanre  11162  climcn2  11250  summodc  11324  prodmodclem2  11518  prodmodc  11519  eirrap  11718  dvds2lem  11743  bezoutlemnewy  11929  bezoutlembi  11938  dvdsmulgcd  11958  divgcdcoprm0  12033  cncongr1  12035  sqrt2irrap  12112  pcqmul  12235  pcneg  12256  pcadd  12271  4sqlem1  12318  4sqlem2  12319  4sqlem4  12322  mul4sq  12324  restbasg  12808  txbas  12898  blin2  13072  xmettxlem  13149  xmettx  13150  addcncntoplem  13191  mulcncf  13231  logbgcd1irr  13525  logbgcd1irrap  13528  2sqlem5  13595  2sqlem9  13600