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  6076  f1o2ndf1  6295  eroveu  6694  eroprf  6696  genipv  7593  genpelvl  7596  genpelvu  7597  genprndl  7605  genprndu  7606  addlocpr  7620  addnqprlemrl  7641  addnqprlemru  7642  mulnqprlemrl  7657  mulnqprlemru  7658  ltsopr  7680  ltaddpr  7681  ltexprlemfl  7693  ltexprlemrl  7694  ltexprlemfu  7695  ltexprlemru  7696  cauappcvgprlemladdfu  7738  cauappcvgprlemladdfl  7739  caucvgprlemdisj  7758  caucvgprlemladdfu  7761  caucvgprprlemdisj  7786  apreap  8631  apreim  8647  apirr  8649  apsym  8650  apcotr  8651  apadd1  8652  apneg  8655  mulext1  8656  apti  8666  aprcl  8690  qapne  9730  qtri3or  10347  exbtwnzlemex  10356  rebtwn2z  10361  cjap  11088  rexanre  11402  climcn2  11491  summodc  11565  prodmodclem2  11759  prodmodc  11760  eirrap  11960  dvds2lem  11985  bezoutlemnewy  12188  bezoutlembi  12197  dvdsmulgcd  12217  divgcdcoprm0  12294  cncongr1  12296  sqrt2irrap  12373  pcqmul  12497  pcneg  12519  pcadd  12534  4sqlem1  12582  4sqlem2  12583  4sqlem4  12586  mul4sq  12588  4sqlem12  12596  4sqlem13m  12597  4sqlem18  12602  imasaddfnlemg  13016  imasmnd2  13154  imasgrp2  13316  imasrng  13588  imasring  13696  dvdsrtr  13733  isnzr2  13816  lss1d  14015  znidom  14289  restbasg  14488  txbas  14578  blin2  14752  xmettxlem  14829  xmettx  14830  addcncntoplem  14881  mulcncf  14928  plyf  15057  plyadd  15071  plymul  15072  plyco  15079  plycj  15081  plycn  15082  plyrecj  15083  dvply2g  15086  logbgcd1irr  15287  logbgcd1irrap  15290  2sqlem5  15444  2sqlem9  15449