Theorem rexlimdvva 2557

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

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 1480  ∃wrex 2417

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-i5r 1515

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-ral 2421  df-rex 2422

This theorem is referenced by:  ovelrn  5919  f1o2ndf1  6125  eroveu  6520  eroprf  6522  genipv  7317  genpelvl  7320  genpelvu  7321  genprndl  7329  genprndu  7330  addlocpr  7344  addnqprlemrl  7365  addnqprlemru  7366  mulnqprlemrl  7381  mulnqprlemru  7382  ltsopr  7404  ltaddpr  7405  ltexprlemfl  7417  ltexprlemrl  7418  ltexprlemfu  7419  ltexprlemru  7420  cauappcvgprlemladdfu  7462  cauappcvgprlemladdfl  7463  caucvgprlemdisj  7482  caucvgprlemladdfu  7485  caucvgprprlemdisj  7510  apreap  8349  apreim  8365  apirr  8367  apsym  8368  apcotr  8369  apadd1  8370  apneg  8373  mulext1  8374  apti  8384  aprcl  8408  qapne  9431  qtri3or  10020  exbtwnzlemex  10027  rebtwn2z  10032  cjap  10678  rexanre  10992  climcn2  11078  summodc  11152  prodmodclem2  11346  prodmodc  11347  eirrap  11484  dvds2lem  11505  bezoutlemnewy  11684  bezoutlembi  11693  dvdsmulgcd  11713  divgcdcoprm0  11782  cncongr1  11784  sqrt2irrap  11858  restbasg  12337  txbas  12427  blin2  12601  xmettxlem  12678  xmettx  12679  addcncntoplem  12720  mulcncf  12760