Theorem rexlimdvva 2600

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2146  ∃wrex 2454

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 1445  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-4 1508  ax-17 1524  ax-ial 1532  ax-i5r 1533

This theorem depends on definitions:  df-bi 117  df-nf 1459  df-ral 2458  df-rex 2459

This theorem is referenced by:  ovelrn  6013  f1o2ndf1  6219  eroveu  6616  eroprf  6618  genipv  7483  genpelvl  7486  genpelvu  7487  genprndl  7495  genprndu  7496  addlocpr  7510  addnqprlemrl  7531  addnqprlemru  7532  mulnqprlemrl  7547  mulnqprlemru  7548  ltsopr  7570  ltaddpr  7571  ltexprlemfl  7583  ltexprlemrl  7584  ltexprlemfu  7585  ltexprlemru  7586  cauappcvgprlemladdfu  7628  cauappcvgprlemladdfl  7629  caucvgprlemdisj  7648  caucvgprlemladdfu  7651  caucvgprprlemdisj  7676  apreap  8518  apreim  8534  apirr  8536  apsym  8537  apcotr  8538  apadd1  8539  apneg  8542  mulext1  8543  apti  8553  aprcl  8577  qapne  9612  qtri3or  10213  exbtwnzlemex  10220  rebtwn2z  10225  cjap  10883  rexanre  11197  climcn2  11285  summodc  11359  prodmodclem2  11553  prodmodc  11554  eirrap  11753  dvds2lem  11778  bezoutlemnewy  11964  bezoutlembi  11973  dvdsmulgcd  11993  divgcdcoprm0  12068  cncongr1  12070  sqrt2irrap  12147  pcqmul  12270  pcneg  12291  pcadd  12306  4sqlem1  12353  4sqlem2  12354  4sqlem4  12357  mul4sq  12359  restbasg  13248  txbas  13338  blin2  13512  xmettxlem  13589  xmettx  13590  addcncntoplem  13631  mulcncf  13671  logbgcd1irr  13965  logbgcd1irrap  13968  2sqlem5  14035  2sqlem9  14040