Theorem rexlimdvva 2658

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

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

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-i5r 1583

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-ral 2515  df-rex 2516

This theorem is referenced by:  ovelrn  6171  f1o2ndf1  6393  eroveu  6795  eroprf  6797  genipv  7729  genpelvl  7732  genpelvu  7733  genprndl  7741  genprndu  7742  addlocpr  7756  addnqprlemrl  7777  addnqprlemru  7778  mulnqprlemrl  7793  mulnqprlemru  7794  ltsopr  7816  ltaddpr  7817  ltexprlemfl  7829  ltexprlemrl  7830  ltexprlemfu  7831  ltexprlemru  7832  cauappcvgprlemladdfu  7874  cauappcvgprlemladdfl  7875  caucvgprlemdisj  7894  caucvgprlemladdfu  7897  caucvgprprlemdisj  7922  apreap  8767  apreim  8783  apirr  8785  apsym  8786  apcotr  8787  apadd1  8788  apneg  8791  mulext1  8792  apti  8802  aprcl  8826  qapne  9873  qtri3or  10501  exbtwnzlemex  10510  rebtwn2z  10515  cjap  11471  rexanre  11785  climcn2  11874  summodc  11949  prodmodclem2  12143  prodmodc  12144  eirrap  12344  dvds2lem  12369  bezoutlemnewy  12572  bezoutlembi  12581  dvdsmulgcd  12601  divgcdcoprm0  12678  cncongr1  12680  sqrt2irrap  12757  pcqmul  12881  pcneg  12903  pcadd  12918  4sqlem1  12966  4sqlem2  12967  4sqlem4  12970  mul4sq  12972  4sqlem12  12980  4sqlem13m  12981  4sqlem18  12986  imasaddfnlemg  13402  imasmnd2  13540  imasgrp2  13702  imasrng  13975  imasring  14083  dvdsrtr  14121  isnzr2  14204  lss1d  14403  znidom  14677  restbasg  14898  txbas  14988  blin2  15162  xmettxlem  15239  xmettx  15240  addcncntoplem  15291  mulcncf  15338  plyf  15467  plyadd  15481  plymul  15482  plyco  15489  plycj  15491  plycn  15492  plyrecj  15493  dvply2g  15496  logbgcd1irr  15697  logbgcd1irrap  15700  2sqlem5  15854  2sqlem9  15859  upgrpredgv  16003  usgredg4  16072  usgr1vr  16105