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  8879  apreim  8895  apirr  8897  apsym  8898  apcotr  8899  apadd1  8900  apneg  8903  mulext1  8904  apti  8914  aprcl  8938  qapne  9992  qtri3or  10627  exbtwnzlemex  10636  rebtwn2z  10641  cjap  11620  rexanre  11934  climcn2  12023  summodc  12098  prodmodclem2  12292  prodmodc  12293  eirrap  12493  dvds2lem  12518  bezoutlemnewy  12721  bezoutlembi  12730  dvdsmulgcd  12750  divgcdcoprm0  12827  cncongr1  12829  sqrt2irrap  12906  pcqmul  13030  pcneg  13052  pcadd  13067  4sqlem1  13115  4sqlem2  13116  4sqlem4  13119  mul4sq  13121  4sqlem12  13129  4sqlem13m  13130  4sqlem18  13135  imasaddfnlemg  13582  imasmnd2  13711  imasgrp2  13867  imasrng  14199  imasring  14311  dvdsrtr  14350  isnzr2  14433  lss1d  14661  znidom  14935  restbasg  15163  txbas  15253  blin2  15427  xmettxlem  15504  xmettx  15505  addcncntoplem  15556  mulcncf  15603  plyf  15732  plyadd  15746  plymul  15747  plyco  15754  plycj  15756  plycn  15757  plyrecj  15758  dvply2g  15761  logbgcd1irr  15962  logbgcd1irrap  15965  2sqlem5  16122  2sqlem9  16127  upgrpredgv  16271  usgredg4  16340  usgr1vr  16373  qdiff  16973