Theorem rexlimdvva 2619

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2164  ∃wrex 2473

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-i5r 1546

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-ral 2477  df-rex 2478

This theorem is referenced by:  ovelrn  6067  f1o2ndf1  6281  eroveu  6680  eroprf  6682  genipv  7569  genpelvl  7572  genpelvu  7573  genprndl  7581  genprndu  7582  addlocpr  7596  addnqprlemrl  7617  addnqprlemru  7618  mulnqprlemrl  7633  mulnqprlemru  7634  ltsopr  7656  ltaddpr  7657  ltexprlemfl  7669  ltexprlemrl  7670  ltexprlemfu  7671  ltexprlemru  7672  cauappcvgprlemladdfu  7714  cauappcvgprlemladdfl  7715  caucvgprlemdisj  7734  caucvgprlemladdfu  7737  caucvgprprlemdisj  7762  apreap  8606  apreim  8622  apirr  8624  apsym  8625  apcotr  8626  apadd1  8627  apneg  8630  mulext1  8631  apti  8641  aprcl  8665  qapne  9704  qtri3or  10310  exbtwnzlemex  10318  rebtwn2z  10323  cjap  11050  rexanre  11364  climcn2  11452  summodc  11526  prodmodclem2  11720  prodmodc  11721  eirrap  11921  dvds2lem  11946  bezoutlemnewy  12133  bezoutlembi  12142  dvdsmulgcd  12162  divgcdcoprm0  12239  cncongr1  12241  sqrt2irrap  12318  pcqmul  12441  pcneg  12463  pcadd  12478  4sqlem1  12526  4sqlem2  12527  4sqlem4  12530  mul4sq  12532  4sqlem12  12540  4sqlem13m  12541  4sqlem18  12546  imasaddfnlemg  12897  imasgrp2  13180  imasrng  13452  imasring  13560  dvdsrtr  13597  isnzr2  13680  lss1d  13879  znidom  14145  restbasg  14336  txbas  14426  blin2  14600  xmettxlem  14677  xmettx  14678  addcncntoplem  14719  mulcncf  14762  plyf  14883  plyadd  14897  plymul  14898  logbgcd1irr  15099  logbgcd1irrap  15102  2sqlem5  15206  2sqlem9  15211