Theorem rexlimdvva 2632

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2177  ∃wrex 2486

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-i5r 1559

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-ral 2490  df-rex 2491

This theorem is referenced by:  ovelrn  6105  f1o2ndf1  6324  eroveu  6723  eroprf  6725  genipv  7635  genpelvl  7638  genpelvu  7639  genprndl  7647  genprndu  7648  addlocpr  7662  addnqprlemrl  7683  addnqprlemru  7684  mulnqprlemrl  7699  mulnqprlemru  7700  ltsopr  7722  ltaddpr  7723  ltexprlemfl  7735  ltexprlemrl  7736  ltexprlemfu  7737  ltexprlemru  7738  cauappcvgprlemladdfu  7780  cauappcvgprlemladdfl  7781  caucvgprlemdisj  7800  caucvgprlemladdfu  7803  caucvgprprlemdisj  7828  apreap  8673  apreim  8689  apirr  8691  apsym  8692  apcotr  8693  apadd1  8694  apneg  8697  mulext1  8698  apti  8708  aprcl  8732  qapne  9773  qtri3or  10396  exbtwnzlemex  10405  rebtwn2z  10410  cjap  11267  rexanre  11581  climcn2  11670  summodc  11744  prodmodclem2  11938  prodmodc  11939  eirrap  12139  dvds2lem  12164  bezoutlemnewy  12367  bezoutlembi  12376  dvdsmulgcd  12396  divgcdcoprm0  12473  cncongr1  12475  sqrt2irrap  12552  pcqmul  12676  pcneg  12698  pcadd  12713  4sqlem1  12761  4sqlem2  12762  4sqlem4  12765  mul4sq  12767  4sqlem12  12775  4sqlem13m  12776  4sqlem18  12781  imasaddfnlemg  13196  imasmnd2  13334  imasgrp2  13496  imasrng  13768  imasring  13876  dvdsrtr  13913  isnzr2  13996  lss1d  14195  znidom  14469  restbasg  14690  txbas  14780  blin2  14954  xmettxlem  15031  xmettx  15032  addcncntoplem  15083  mulcncf  15130  plyf  15259  plyadd  15273  plymul  15274  plyco  15281  plycj  15283  plycn  15284  plyrecj  15285  dvply2g  15288  logbgcd1irr  15489  logbgcd1irrap  15492  2sqlem5  15646  2sqlem9  15651