Theorem rexlimdvva 2589

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

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 2135  ∃wrex 2443

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 1434  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-4 1497  ax-17 1513  ax-ial 1521  ax-i5r 1522

This theorem depends on definitions:  df-bi 116  df-nf 1448  df-ral 2447  df-rex 2448

This theorem is referenced by:  ovelrn  5981  f1o2ndf1  6187  eroveu  6583  eroprf  6585  genipv  7441  genpelvl  7444  genpelvu  7445  genprndl  7453  genprndu  7454  addlocpr  7468  addnqprlemrl  7489  addnqprlemru  7490  mulnqprlemrl  7505  mulnqprlemru  7506  ltsopr  7528  ltaddpr  7529  ltexprlemfl  7541  ltexprlemrl  7542  ltexprlemfu  7543  ltexprlemru  7544  cauappcvgprlemladdfu  7586  cauappcvgprlemladdfl  7587  caucvgprlemdisj  7606  caucvgprlemladdfu  7609  caucvgprprlemdisj  7634  apreap  8476  apreim  8492  apirr  8494  apsym  8495  apcotr  8496  apadd1  8497  apneg  8500  mulext1  8501  apti  8511  aprcl  8535  qapne  9568  qtri3or  10168  exbtwnzlemex  10175  rebtwn2z  10180  cjap  10834  rexanre  11148  climcn2  11236  summodc  11310  prodmodclem2  11504  prodmodc  11505  eirrap  11704  dvds2lem  11729  bezoutlemnewy  11914  bezoutlembi  11923  dvdsmulgcd  11943  divgcdcoprm0  12012  cncongr1  12014  sqrt2irrap  12091  pcqmul  12214  pcneg  12235  pcadd  12250  restbasg  12715  txbas  12805  blin2  12979  xmettxlem  13056  xmettx  13057  addcncntoplem  13098  mulcncf  13138  logbgcd1irr  13432  logbgcd1irrap  13435