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  7595  genpelvl  7598  genpelvu  7599  genprndl  7607  genprndu  7608  addlocpr  7622  addnqprlemrl  7643  addnqprlemru  7644  mulnqprlemrl  7659  mulnqprlemru  7660  ltsopr  7682  ltaddpr  7683  ltexprlemfl  7695  ltexprlemrl  7696  ltexprlemfu  7697  ltexprlemru  7698  cauappcvgprlemladdfu  7740  cauappcvgprlemladdfl  7741  caucvgprlemdisj  7760  caucvgprlemladdfu  7763  caucvgprprlemdisj  7788  apreap  8633  apreim  8649  apirr  8651  apsym  8652  apcotr  8653  apadd1  8654  apneg  8657  mulext1  8658  apti  8668  aprcl  8692  qapne  9732  qtri3or  10349  exbtwnzlemex  10358  rebtwn2z  10363  cjap  11090  rexanre  11404  climcn2  11493  summodc  11567  prodmodclem2  11761  prodmodc  11762  eirrap  11962  dvds2lem  11987  bezoutlemnewy  12190  bezoutlembi  12199  dvdsmulgcd  12219  divgcdcoprm0  12296  cncongr1  12298  sqrt2irrap  12375  pcqmul  12499  pcneg  12521  pcadd  12536  4sqlem1  12584  4sqlem2  12585  4sqlem4  12588  mul4sq  12590  4sqlem12  12598  4sqlem13m  12599  4sqlem18  12604  imasaddfnlemg  13018  imasmnd2  13156  imasgrp2  13318  imasrng  13590  imasring  13698  dvdsrtr  13735  isnzr2  13818  lss1d  14017  znidom  14291  restbasg  14512  txbas  14602  blin2  14776  xmettxlem  14853  xmettx  14854  addcncntoplem  14905  mulcncf  14952  plyf  15081  plyadd  15095  plymul  15096  plyco  15103  plycj  15105  plycn  15106  plyrecj  15107  dvply2g  15110  logbgcd1irr  15311  logbgcd1irrap  15314  2sqlem5  15468  2sqlem9  15473