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  6163  f1o2ndf1  6385  eroveu  6786  eroprf  6788  genipv  7712  genpelvl  7715  genpelvu  7716  genprndl  7724  genprndu  7725  addlocpr  7739  addnqprlemrl  7760  addnqprlemru  7761  mulnqprlemrl  7776  mulnqprlemru  7777  ltsopr  7799  ltaddpr  7800  ltexprlemfl  7812  ltexprlemrl  7813  ltexprlemfu  7814  ltexprlemru  7815  cauappcvgprlemladdfu  7857  cauappcvgprlemladdfl  7858  caucvgprlemdisj  7877  caucvgprlemladdfu  7880  caucvgprprlemdisj  7905  apreap  8750  apreim  8766  apirr  8768  apsym  8769  apcotr  8770  apadd1  8771  apneg  8774  mulext1  8775  apti  8785  aprcl  8809  qapne  9851  qtri3or  10477  exbtwnzlemex  10486  rebtwn2z  10491  cjap  11438  rexanre  11752  climcn2  11841  summodc  11915  prodmodclem2  12109  prodmodc  12110  eirrap  12310  dvds2lem  12335  bezoutlemnewy  12538  bezoutlembi  12547  dvdsmulgcd  12567  divgcdcoprm0  12644  cncongr1  12646  sqrt2irrap  12723  pcqmul  12847  pcneg  12869  pcadd  12884  4sqlem1  12932  4sqlem2  12933  4sqlem4  12936  mul4sq  12938  4sqlem12  12946  4sqlem13m  12947  4sqlem18  12952  imasaddfnlemg  13368  imasmnd2  13506  imasgrp2  13668  imasrng  13940  imasring  14048  dvdsrtr  14086  isnzr2  14169  lss1d  14368  znidom  14642  restbasg  14863  txbas  14953  blin2  15127  xmettxlem  15204  xmettx  15205  addcncntoplem  15256  mulcncf  15303  plyf  15432  plyadd  15446  plymul  15447  plyco  15454  plycj  15456  plycn  15457  plyrecj  15458  dvply2g  15461  logbgcd1irr  15662  logbgcd1irrap  15665  2sqlem5  15819  2sqlem9  15824  upgrpredgv  15965  usgredg4  16034  usgr1vr  16067