Theorem rexlimdvva 2656

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2200  ∃wrex 2509

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-i5r 1581

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-ral 2513  df-rex 2514

This theorem is referenced by:  ovelrn  6166  f1o2ndf1  6388  eroveu  6790  eroprf  6792  genipv  7722  genpelvl  7725  genpelvu  7726  genprndl  7734  genprndu  7735  addlocpr  7749  addnqprlemrl  7770  addnqprlemru  7771  mulnqprlemrl  7786  mulnqprlemru  7787  ltsopr  7809  ltaddpr  7810  ltexprlemfl  7822  ltexprlemrl  7823  ltexprlemfu  7824  ltexprlemru  7825  cauappcvgprlemladdfu  7867  cauappcvgprlemladdfl  7868  caucvgprlemdisj  7887  caucvgprlemladdfu  7890  caucvgprprlemdisj  7915  apreap  8760  apreim  8776  apirr  8778  apsym  8779  apcotr  8780  apadd1  8781  apneg  8784  mulext1  8785  apti  8795  aprcl  8819  qapne  9866  qtri3or  10493  exbtwnzlemex  10502  rebtwn2z  10507  cjap  11460  rexanre  11774  climcn2  11863  summodc  11937  prodmodclem2  12131  prodmodc  12132  eirrap  12332  dvds2lem  12357  bezoutlemnewy  12560  bezoutlembi  12569  dvdsmulgcd  12589  divgcdcoprm0  12666  cncongr1  12668  sqrt2irrap  12745  pcqmul  12869  pcneg  12891  pcadd  12906  4sqlem1  12954  4sqlem2  12955  4sqlem4  12958  mul4sq  12960  4sqlem12  12968  4sqlem13m  12969  4sqlem18  12974  imasaddfnlemg  13390  imasmnd2  13528  imasgrp2  13690  imasrng  13962  imasring  14070  dvdsrtr  14108  isnzr2  14191  lss1d  14390  znidom  14664  restbasg  14885  txbas  14975  blin2  15149  xmettxlem  15226  xmettx  15227  addcncntoplem  15278  mulcncf  15325  plyf  15454  plyadd  15468  plymul  15469  plyco  15476  plycj  15478  plycn  15479  plyrecj  15480  dvply2g  15483  logbgcd1irr  15684  logbgcd1irrap  15687  2sqlem5  15841  2sqlem9  15846  upgrpredgv  15990  usgredg4  16059  usgr1vr  16092