Theorem rexlimdvva 2656

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2200  ∃wrex 2509

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-i5r 1581

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-ral 2513  df-rex 2514

This theorem is referenced by:  ovelrn  6145  f1o2ndf1  6364  eroveu  6763  eroprf  6765  genipv  7684  genpelvl  7687  genpelvu  7688  genprndl  7696  genprndu  7697  addlocpr  7711  addnqprlemrl  7732  addnqprlemru  7733  mulnqprlemrl  7748  mulnqprlemru  7749  ltsopr  7771  ltaddpr  7772  ltexprlemfl  7784  ltexprlemrl  7785  ltexprlemfu  7786  ltexprlemru  7787  cauappcvgprlemladdfu  7829  cauappcvgprlemladdfl  7830  caucvgprlemdisj  7849  caucvgprlemladdfu  7852  caucvgprprlemdisj  7877  apreap  8722  apreim  8738  apirr  8740  apsym  8741  apcotr  8742  apadd1  8743  apneg  8746  mulext1  8747  apti  8757  aprcl  8781  qapne  9822  qtri3or  10447  exbtwnzlemex  10456  rebtwn2z  10461  cjap  11403  rexanre  11717  climcn2  11806  summodc  11880  prodmodclem2  12074  prodmodc  12075  eirrap  12275  dvds2lem  12300  bezoutlemnewy  12503  bezoutlembi  12512  dvdsmulgcd  12532  divgcdcoprm0  12609  cncongr1  12611  sqrt2irrap  12688  pcqmul  12812  pcneg  12834  pcadd  12849  4sqlem1  12897  4sqlem2  12898  4sqlem4  12901  mul4sq  12903  4sqlem12  12911  4sqlem13m  12912  4sqlem18  12917  imasaddfnlemg  13333  imasmnd2  13471  imasgrp2  13633  imasrng  13905  imasring  14013  dvdsrtr  14050  isnzr2  14133  lss1d  14332  znidom  14606  restbasg  14827  txbas  14917  blin2  15091  xmettxlem  15168  xmettx  15169  addcncntoplem  15220  mulcncf  15267  plyf  15396  plyadd  15410  plymul  15411  plyco  15418  plycj  15420  plycn  15421  plyrecj  15422  dvply2g  15425  logbgcd1irr  15626  logbgcd1irrap  15629  2sqlem5  15783  2sqlem9  15788  upgrpredgv  15929  usgredg4  15998