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  6160  f1o2ndf1  6380  eroveu  6781  eroprf  6783  genipv  7704  genpelvl  7707  genpelvu  7708  genprndl  7716  genprndu  7717  addlocpr  7731  addnqprlemrl  7752  addnqprlemru  7753  mulnqprlemrl  7768  mulnqprlemru  7769  ltsopr  7791  ltaddpr  7792  ltexprlemfl  7804  ltexprlemrl  7805  ltexprlemfu  7806  ltexprlemru  7807  cauappcvgprlemladdfu  7849  cauappcvgprlemladdfl  7850  caucvgprlemdisj  7869  caucvgprlemladdfu  7872  caucvgprprlemdisj  7897  apreap  8742  apreim  8758  apirr  8760  apsym  8761  apcotr  8762  apadd1  8763  apneg  8766  mulext1  8767  apti  8777  aprcl  8801  qapne  9842  qtri3or  10468  exbtwnzlemex  10477  rebtwn2z  10482  cjap  11425  rexanre  11739  climcn2  11828  summodc  11902  prodmodclem2  12096  prodmodc  12097  eirrap  12297  dvds2lem  12322  bezoutlemnewy  12525  bezoutlembi  12534  dvdsmulgcd  12554  divgcdcoprm0  12631  cncongr1  12633  sqrt2irrap  12710  pcqmul  12834  pcneg  12856  pcadd  12871  4sqlem1  12919  4sqlem2  12920  4sqlem4  12923  mul4sq  12925  4sqlem12  12933  4sqlem13m  12934  4sqlem18  12939  imasaddfnlemg  13355  imasmnd2  13493  imasgrp2  13655  imasrng  13927  imasring  14035  dvdsrtr  14073  isnzr2  14156  lss1d  14355  znidom  14629  restbasg  14850  txbas  14940  blin2  15114  xmettxlem  15191  xmettx  15192  addcncntoplem  15243  mulcncf  15290  plyf  15419  plyadd  15433  plymul  15434  plyco  15441  plycj  15443  plycn  15444  plyrecj  15445  dvply2g  15448  logbgcd1irr  15649  logbgcd1irrap  15652  2sqlem5  15806  2sqlem9  15811  upgrpredgv  15952  usgredg4  16021