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  6238  f1o2ndf1  6464  eroveu  6900  eroprf  6902  genipv  7876  genpelvl  7879  genpelvu  7880  genprndl  7888  genprndu  7889  addlocpr  7903  addnqprlemrl  7924  addnqprlemru  7925  mulnqprlemrl  7940  mulnqprlemru  7941  ltsopr  7963  ltaddpr  7964  ltexprlemfl  7976  ltexprlemrl  7977  ltexprlemfu  7978  ltexprlemru  7979  cauappcvgprlemladdfu  8021  cauappcvgprlemladdfl  8022  caucvgprlemdisj  8041  caucvgprlemladdfu  8044  caucvgprprlemdisj  8069  apreap  8916  apreim  8932  apirr  8934  apsym  8935  apcotr  8936  apadd1  8937  apneg  8940  mulext1  8941  apti  8951  aprcl  8975  qapne  10041  qtri3or  10677  exbtwnzlemex  10686  rebtwn2z  10691  cjap  11674  rexanre  11988  climcn2  12077  summodc  12152  prodmodclem2  12346  prodmodc  12347  eirrap  12547  dvds2lem  12572  bezoutlemnewy  12775  bezoutlembi  12784  dvdsmulgcd  12804  divgcdcoprm0  12881  cncongr1  12883  sqrt2irrap  12960  pcqmul  13084  pcneg  13106  pcadd  13121  4sqlem1  13169  4sqlem2  13170  4sqlem4  13173  mul4sq  13175  4sqlem12  13183  4sqlem13m  13184  4sqlem18  13189  imasaddfnlemg  13637  imasmnd2  13761  imasgrp2  13915  imasrng  14257  imasring  14371  dvdsrtr  14410  isnzr2  14493  lss1d  14722  znidom  14994  restbasg  15271  txbas  15361  blin2  15535  xmettxlem  15612  xmettx  15613  addcncntoplem  15664  mulcncf  15711  plyf  15840  plyadd  15854  plymul  15855  plyco  15862  plycj  15864  plycn  15865  plyrecj  15866  dvply2g  15869  logbgcd1irr  16075  logbgcd1irrap  16078  2sqlem5  16250  2sqlem9  16255  upgrpredgv  16399  usgredg4  16468  usgr1vr  16501  qdiff  17110