Theorem rexlimdvva 2622

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2167  ∃wrex 2476

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-i5r 1549

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-ral 2480  df-rex 2481

This theorem is referenced by:  ovelrn  6072  f1o2ndf1  6286  eroveu  6685  eroprf  6687  genipv  7576  genpelvl  7579  genpelvu  7580  genprndl  7588  genprndu  7589  addlocpr  7603  addnqprlemrl  7624  addnqprlemru  7625  mulnqprlemrl  7640  mulnqprlemru  7641  ltsopr  7663  ltaddpr  7664  ltexprlemfl  7676  ltexprlemrl  7677  ltexprlemfu  7678  ltexprlemru  7679  cauappcvgprlemladdfu  7721  cauappcvgprlemladdfl  7722  caucvgprlemdisj  7741  caucvgprlemladdfu  7744  caucvgprprlemdisj  7769  apreap  8614  apreim  8630  apirr  8632  apsym  8633  apcotr  8634  apadd1  8635  apneg  8638  mulext1  8639  apti  8649  aprcl  8673  qapne  9713  qtri3or  10330  exbtwnzlemex  10339  rebtwn2z  10344  cjap  11071  rexanre  11385  climcn2  11474  summodc  11548  prodmodclem2  11742  prodmodc  11743  eirrap  11943  dvds2lem  11968  bezoutlemnewy  12163  bezoutlembi  12172  dvdsmulgcd  12192  divgcdcoprm0  12269  cncongr1  12271  sqrt2irrap  12348  pcqmul  12472  pcneg  12494  pcadd  12509  4sqlem1  12557  4sqlem2  12558  4sqlem4  12561  mul4sq  12563  4sqlem12  12571  4sqlem13m  12572  4sqlem18  12577  imasaddfnlemg  12957  imasgrp2  13240  imasrng  13512  imasring  13620  dvdsrtr  13657  isnzr2  13740  lss1d  13939  znidom  14213  restbasg  14404  txbas  14494  blin2  14668  xmettxlem  14745  xmettx  14746  addcncntoplem  14797  mulcncf  14844  plyf  14973  plyadd  14987  plymul  14988  plyco  14995  plycj  14997  plycn  14998  plyrecj  14999  dvply2g  15002  logbgcd1irr  15203  logbgcd1irrap  15206  2sqlem5  15360  2sqlem9  15365