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  7877  genpelvl  7880  genpelvu  7881  genprndl  7889  genprndu  7890  addlocpr  7904  addnqprlemrl  7925  addnqprlemru  7926  mulnqprlemrl  7941  mulnqprlemru  7942  ltsopr  7964  ltaddpr  7965  ltexprlemfl  7977  ltexprlemrl  7978  ltexprlemfu  7979  ltexprlemru  7980  cauappcvgprlemladdfu  8022  cauappcvgprlemladdfl  8023  caucvgprlemdisj  8042  caucvgprlemladdfu  8045  caucvgprprlemdisj  8070  apreap  8918  apreim  8934  apirr  8936  apsym  8937  apcotr  8938  apadd1  8939  apneg  8942  mulext1  8943  apti  8953  aprcl  8977  qapne  10049  qtri3or  10686  exbtwnzlemex  10695  rebtwn2z  10700  cjap  11687  rexanre  12002  climcn2  12093  summodc  12168  prodmodclem2  12362  prodmodc  12363  eirrap  12563  dvds2lem  12588  bezoutlemnewy  12791  bezoutlembi  12800  dvdsmulgcd  12820  divgcdcoprm0  12897  cncongr1  12899  sqrt2irrap  12978  pcqmul  13104  pcneg  13126  pcadd  13141  4sqlem1  13189  4sqlem2  13190  4sqlem4  13193  mul4sq  13195  4sqlem12  13203  4sqlem13m  13204  4sqlem18  13209  imasaddfnlemg  13686  imasmnd2  13810  imasgrp2  13964  imasrng  14306  imasring  14420  dvdsrtr  14459  isnzr2  14542  lss1d  14771  znidom  15043  restbasg  15321  txbas  15411  blin2  15585  xmettxlem  15662  xmettx  15663  addcncntoplem  15714  mulcncf  15761  plyf  15890  plyadd  15904  plymul  15905  plyco  15912  plycj  15914  plycn  15915  plyrecj  15916  dvply2g  15919  logbgcd1irr  16125  logbgcd1irrap  16128  zprmlogbap  16140  2sqlem5  16360  2sqlem9  16365  upgrpredgv  16509  usgredg4  16578  usgr1vr  16611  qdiff  17220