Theorem rexlimdvva 2531

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 114	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝜓 → 𝜒)))
3	2	rexlimdvv 2530	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 → 𝜒))

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 1463  ∃wrex 2391

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-4 1470  ax-17 1489  ax-ial 1497  ax-i5r 1498

This theorem depends on definitions:  df-bi 116  df-nf 1420  df-ral 2395  df-rex 2396

This theorem is referenced by:  ovelrn  5873  f1o2ndf1  6079  eroveu  6474  eroprf  6476  genipv  7265  genpelvl  7268  genpelvu  7269  genprndl  7277  genprndu  7278  addlocpr  7292  addnqprlemrl  7313  addnqprlemru  7314  mulnqprlemrl  7329  mulnqprlemru  7330  ltsopr  7352  ltaddpr  7353  ltexprlemfl  7365  ltexprlemrl  7366  ltexprlemfu  7367  ltexprlemru  7368  cauappcvgprlemladdfu  7410  cauappcvgprlemladdfl  7411  caucvgprlemdisj  7430  caucvgprlemladdfu  7433  caucvgprprlemdisj  7458  apreap  8267  apreim  8283  apirr  8285  apsym  8286  apcotr  8287  apadd1  8288  apneg  8291  mulext1  8292  apti  8302  qapne  9333  qtri3or  9913  exbtwnzlemex  9920  rebtwn2z  9925  cjap  10571  rexanre  10884  climcn2  10970  summodc  11044  eirrap  11332  dvds2lem  11353  bezoutlemnewy  11530  bezoutlembi  11539  dvdsmulgcd  11559  divgcdcoprm0  11628  cncongr1  11630  sqrt2irrap  11703  restbasg  12180  txbas  12269  blin2  12421  xmettxlem  12498  xmettx  12499  addcncntoplem  12537  mulcncf  12577