Theorem rexlimdvva 2676

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2209  ∃wrex 2529

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-i5r 1588

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533  df-rex 2534

This theorem is referenced by:  ovelrn  6232  f1o2ndf1  6458  eroveu  6894  eroprf  6896  genipv  7870  genpelvl  7873  genpelvu  7874  genprndl  7882  genprndu  7883  addlocpr  7897  addnqprlemrl  7918  addnqprlemru  7919  mulnqprlemrl  7934  mulnqprlemru  7935  ltsopr  7957  ltaddpr  7958  ltexprlemfl  7970  ltexprlemrl  7971  ltexprlemfu  7972  ltexprlemru  7973  cauappcvgprlemladdfu  8015  cauappcvgprlemladdfl  8016  caucvgprlemdisj  8035  caucvgprlemladdfu  8038  caucvgprprlemdisj  8063  apreap  8909  apreim  8925  apirr  8927  apsym  8928  apcotr  8929  apadd1  8930  apneg  8933  mulext1  8934  apti  8944  aprcl  8968  qapne  10022  qtri3or  10658  exbtwnzlemex  10667  rebtwn2z  10672  cjap  11655  rexanre  11969  climcn2  12058  summodc  12133  prodmodclem2  12327  prodmodc  12328  eirrap  12528  dvds2lem  12553  bezoutlemnewy  12756  bezoutlembi  12765  dvdsmulgcd  12785  divgcdcoprm0  12862  cncongr1  12864  sqrt2irrap  12941  pcqmul  13065  pcneg  13087  pcadd  13102  4sqlem1  13150  4sqlem2  13151  4sqlem4  13154  mul4sq  13156  4sqlem12  13164  4sqlem13m  13165  4sqlem18  13170  imasaddfnlemg  13618  imasmnd2  13742  imasgrp2  13896  imasrng  14238  imasring  14352  dvdsrtr  14391  isnzr2  14474  lss1d  14703  znidom  14975  restbasg  15252  txbas  15342  blin2  15516  xmettxlem  15593  xmettx  15594  addcncntoplem  15645  mulcncf  15692  plyf  15821  plyadd  15835  plymul  15836  plyco  15843  plycj  15845  plycn  15846  plyrecj  15847  dvply2g  15850  logbgcd1irr  16052  logbgcd1irrap  16055  2sqlem5  16221  2sqlem9  16226  upgrpredgv  16370  usgredg4  16439  usgr1vr  16472  qdiff  17072