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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∈ wcel 2209  ∃wrex 2529

This proof depends on 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 proof depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533  df-rex 2534

This theorem is used by:  ovelrn  6241  f1o2ndf1  6468  eroveu  6905  eroprf  6907  genipv  7883  genpelvl  7886  genpelvu  7887  genprndl  7895  genprndu  7896  addlocpr  7910  addnqprlemrl  7931  addnqprlemru  7932  mulnqprlemrl  7947  mulnqprlemru  7948  ltsopr  7970  ltaddpr  7971  ltexprlemfl  7983  ltexprlemrl  7984  ltexprlemfu  7985  ltexprlemru  7986  cauappcvgprlemladdfu  8028  cauappcvgprlemladdfl  8029  caucvgprlemdisj  8048  caucvgprlemladdfu  8051  caucvgprprlemdisj  8076  apreap  8924  apreim  8940  apirr  8942  apsym  8943  apcotr  8944  apadd1  8945  apneg  8948  mulext1  8949  apti  8959  aprcl  8983  qapne  10055  qtri3or  10692  exbtwnzlemex  10701  rebtwn2z  10706  cjap  11694  rexanre  12009  climcn2  12100  summodc  12175  prodmodclem2  12369  prodmodc  12370  eirrap  12570  dvds2lem  12595  bezoutlemnewy  12798  bezoutlembi  12807  dvdsmulgcd  12827  divgcdcoprm0  12904  cncongr1  12906  sqrt2irrap  12985  pcqmul  13111  pcneg  13133  pcadd  13148  4sqlem1  13196  4sqlem2  13197  4sqlem4  13200  mul4sq  13202  4sqlem12  13210  4sqlem13m  13211  4sqlem18  13216  imasaddfnlemg  13694  imasmnd2  13818  imasgrp2  13972  imasrng  14362  imasring  14478  dvdsrtr  14517  isnzr2  14600  lss1d  14829  znidom  15101  restbasg  15427  txbas  15517  blin2  15691  xmettxlem  15768  xmettx  15769  addcncntoplem  15820  mulcncf  15867  plyf  15996  plyadd  16010  plymul  16011  plyco  16018  plycj  16020  plycn  16021  plyrecj  16022  dvply2g  16025  logbgcd1irr  16236  logbgcd1irrap  16239  zprmlogbap  16251  2sqlem5  16476  2sqlem9  16481  upgrpredgv  16625  usgredg4  16694  usgr1vr  16727  qdiff  17338