Theorem rexlimdvva 2602

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2148  ∃wrex 2456

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-i5r 1535

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-ral 2460  df-rex 2461

This theorem is referenced by:  ovelrn  6023  f1o2ndf1  6229  eroveu  6626  eroprf  6628  genipv  7508  genpelvl  7511  genpelvu  7512  genprndl  7520  genprndu  7521  addlocpr  7535  addnqprlemrl  7556  addnqprlemru  7557  mulnqprlemrl  7572  mulnqprlemru  7573  ltsopr  7595  ltaddpr  7596  ltexprlemfl  7608  ltexprlemrl  7609  ltexprlemfu  7610  ltexprlemru  7611  cauappcvgprlemladdfu  7653  cauappcvgprlemladdfl  7654  caucvgprlemdisj  7673  caucvgprlemladdfu  7676  caucvgprprlemdisj  7701  apreap  8544  apreim  8560  apirr  8562  apsym  8563  apcotr  8564  apadd1  8565  apneg  8568  mulext1  8569  apti  8579  aprcl  8603  qapne  9639  qtri3or  10243  exbtwnzlemex  10250  rebtwn2z  10255  cjap  10915  rexanre  11229  climcn2  11317  summodc  11391  prodmodclem2  11585  prodmodc  11586  eirrap  11785  dvds2lem  11810  bezoutlemnewy  11997  bezoutlembi  12006  dvdsmulgcd  12026  divgcdcoprm0  12101  cncongr1  12103  sqrt2irrap  12180  pcqmul  12303  pcneg  12324  pcadd  12339  4sqlem1  12386  4sqlem2  12387  4sqlem4  12390  mul4sq  12392  imasaddfnlemg  12735  dvdsrtr  13270  restbasg  13671  txbas  13761  blin2  13935  xmettxlem  14012  xmettx  14013  addcncntoplem  14054  mulcncf  14094  logbgcd1irr  14388  logbgcd1irrap  14391  2sqlem5  14469  2sqlem9  14474