Theorem rexlimdvva 2670

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2205  ∃wrex 2523

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 2527  df-rex 2528

This theorem is referenced by:  ovelrn  6211  f1o2ndf1  6437  eroveu  6873  eroprf  6875  genipv  7840  genpelvl  7843  genpelvu  7844  genprndl  7852  genprndu  7853  addlocpr  7867  addnqprlemrl  7888  addnqprlemru  7889  mulnqprlemrl  7904  mulnqprlemru  7905  ltsopr  7927  ltaddpr  7928  ltexprlemfl  7940  ltexprlemrl  7941  ltexprlemfu  7942  ltexprlemru  7943  cauappcvgprlemladdfu  7985  cauappcvgprlemladdfl  7986  caucvgprlemdisj  8005  caucvgprlemladdfu  8008  caucvgprprlemdisj  8033  apreap  8878  apreim  8894  apirr  8896  apsym  8897  apcotr  8898  apadd1  8899  apneg  8902  mulext1  8903  apti  8913  aprcl  8937  qapne  9989  qtri3or  10624  exbtwnzlemex  10633  rebtwn2z  10638  cjap  11616  rexanre  11930  climcn2  12019  summodc  12094  prodmodclem2  12288  prodmodc  12289  eirrap  12489  dvds2lem  12514  bezoutlemnewy  12717  bezoutlembi  12726  dvdsmulgcd  12746  divgcdcoprm0  12823  cncongr1  12825  sqrt2irrap  12902  pcqmul  13026  pcneg  13048  pcadd  13063  4sqlem1  13111  4sqlem2  13112  4sqlem4  13115  mul4sq  13117  4sqlem12  13125  4sqlem13m  13126  4sqlem18  13131  imasaddfnlemg  13611  imasmnd2  13749  imasgrp2  13911  imasrng  14184  imasring  14292  dvdsrtr  14331  isnzr2  14414  lss1d  14643  znidom  14917  restbasg  15145  txbas  15235  blin2  15409  xmettxlem  15486  xmettx  15487  addcncntoplem  15538  mulcncf  15585  plyf  15714  plyadd  15728  plymul  15729  plyco  15736  plycj  15738  plycn  15739  plyrecj  15740  dvply2g  15743  logbgcd1irr  15944  logbgcd1irrap  15947  2sqlem5  16104  2sqlem9  16109  upgrpredgv  16253  usgredg4  16322  usgr1vr  16355  qdiff  16945