Theorem rexlimdvva 2659

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2202  ∃wrex 2512

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-i5r 1584

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-ral 2516  df-rex 2517

This theorem is referenced by:  ovelrn  6181  f1o2ndf1  6402  eroveu  6838  eroprf  6840  genipv  7772  genpelvl  7775  genpelvu  7776  genprndl  7784  genprndu  7785  addlocpr  7799  addnqprlemrl  7820  addnqprlemru  7821  mulnqprlemrl  7836  mulnqprlemru  7837  ltsopr  7859  ltaddpr  7860  ltexprlemfl  7872  ltexprlemrl  7873  ltexprlemfu  7874  ltexprlemru  7875  cauappcvgprlemladdfu  7917  cauappcvgprlemladdfl  7918  caucvgprlemdisj  7937  caucvgprlemladdfu  7940  caucvgprprlemdisj  7965  apreap  8810  apreim  8826  apirr  8828  apsym  8829  apcotr  8830  apadd1  8831  apneg  8834  mulext1  8835  apti  8845  aprcl  8869  qapne  9916  qtri3or  10544  exbtwnzlemex  10553  rebtwn2z  10558  cjap  11527  rexanre  11841  climcn2  11930  summodc  12005  prodmodclem2  12199  prodmodc  12200  eirrap  12400  dvds2lem  12425  bezoutlemnewy  12628  bezoutlembi  12637  dvdsmulgcd  12657  divgcdcoprm0  12734  cncongr1  12736  sqrt2irrap  12813  pcqmul  12937  pcneg  12959  pcadd  12974  4sqlem1  13022  4sqlem2  13023  4sqlem4  13026  mul4sq  13028  4sqlem12  13036  4sqlem13m  13037  4sqlem18  13042  imasaddfnlemg  13458  imasmnd2  13596  imasgrp2  13758  imasrng  14031  imasring  14139  dvdsrtr  14177  isnzr2  14260  lss1d  14459  znidom  14733  restbasg  14959  txbas  15049  blin2  15223  xmettxlem  15300  xmettx  15301  addcncntoplem  15352  mulcncf  15399  plyf  15528  plyadd  15542  plymul  15543  plyco  15550  plycj  15552  plycn  15553  plyrecj  15554  dvply2g  15557  logbgcd1irr  15758  logbgcd1irrap  15761  2sqlem5  15918  2sqlem9  15923  upgrpredgv  16067  usgredg4  16136  usgr1vr  16169  qdiff  16761