Theorem rexlimdvva 2676

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∈ wcel 2209  ∃wrex 2529

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-i5r 1588

This proof depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533  df-rex 2534

This theorem is used by:  ovelrn  6241  f1o2ndf1  6468  eroveu  6904  eroprf  6906  genipv  7883  genpelvl  7886  genpelvu  7887  genprndl  7895  genprndu  7896  addlocpr  7910  addnqprlemrl  7931  addnqprlemru  7932  mulnqprlemrl  7947  mulnqprlemru  7948  ltsopr  7970  ltaddpr  7971  ltexprlemfl  7983  ltexprlemrl  7984  ltexprlemfu  7985  ltexprlemru  7986  cauappcvgprlemladdfu  8028  cauappcvgprlemladdfl  8029  caucvgprlemdisj  8048  caucvgprlemladdfu  8051  caucvgprprlemdisj  8076  apreap  8924  apreim  8940  apirr  8942  apsym  8943  apcotr  8944  apadd1  8945  apneg  8948  mulext1  8949  apti  8959  aprcl  8983  qapne  10056  qtri3or  10693  exbtwnzlemex  10702  rebtwn2z  10707  cjap  11695  rexanre  12010  climcn2  12101  summodc  12176  prodmodclem2  12370  prodmodc  12371  eirrap  12571  dvds2lem  12596  bezoutlemnewy  12799  bezoutlembi  12808  dvdsmulgcd  12828  divgcdcoprm0  12905  cncongr1  12907  sqrt2irrap  12986  pcqmul  13112  pcneg  13134  pcadd  13149  4sqlem1  13197  4sqlem2  13198  4sqlem4  13201  mul4sq  13203  4sqlem12  13211  4sqlem13m  13212  4sqlem18  13217  imasaddfnlemg  13695  imasmnd2  13819  imasgrp2  13973  imasrng  14363  imasring  14479  dvdsrtr  14518  isnzr2  14601  lss1d  14830  znidom  15102  restbasg  15406  txbas  15496  blin2  15670  xmettxlem  15747  xmettx  15748  addcncntoplem  15799  mulcncf  15846  plyf  15975  plyadd  15989  plymul  15990  plyco  15997  plycj  15999  plycn  16000  plyrecj  16001  dvply2g  16004  logbgcd1irr  16215  logbgcd1irrap  16218  zprmlogbap  16230  2sqlem5  16455  2sqlem9  16460  upgrpredgv  16604  usgredg4  16673  usgr1vr  16706  qdiff  17317