ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  rexlimdvva GIF version

Theorem rexlimdvva 2560
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
StepHypRef Expression
1 rexlimdvva.1 . . 3 ((𝜑 ∧ (𝑥𝐴𝑦𝐵)) → (𝜓𝜒))
21ex 114 . 2 (𝜑 → ((𝑥𝐴𝑦𝐵) → (𝜓𝜒)))
32rexlimdvv 2559 1 (𝜑 → (∃𝑥𝐴𝑦𝐵 𝜓𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wcel 1481  wrex 2418
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 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-17 1507  ax-ial 1515  ax-i5r 1516
This theorem depends on definitions:  df-bi 116  df-nf 1438  df-ral 2422  df-rex 2423
This theorem is referenced by:  ovelrn  5926  f1o2ndf1  6132  eroveu  6527  eroprf  6529  genipv  7340  genpelvl  7343  genpelvu  7344  genprndl  7352  genprndu  7353  addlocpr  7367  addnqprlemrl  7388  addnqprlemru  7389  mulnqprlemrl  7404  mulnqprlemru  7405  ltsopr  7427  ltaddpr  7428  ltexprlemfl  7440  ltexprlemrl  7441  ltexprlemfu  7442  ltexprlemru  7443  cauappcvgprlemladdfu  7485  cauappcvgprlemladdfl  7486  caucvgprlemdisj  7505  caucvgprlemladdfu  7508  caucvgprprlemdisj  7533  apreap  8372  apreim  8388  apirr  8390  apsym  8391  apcotr  8392  apadd1  8393  apneg  8396  mulext1  8397  apti  8407  aprcl  8431  qapne  9457  qtri3or  10050  exbtwnzlemex  10057  rebtwn2z  10062  cjap  10709  rexanre  11023  climcn2  11109  summodc  11183  prodmodclem2  11377  prodmodc  11378  eirrap  11518  dvds2lem  11539  bezoutlemnewy  11718  bezoutlembi  11727  dvdsmulgcd  11747  divgcdcoprm0  11816  cncongr1  11818  sqrt2irrap  11892  restbasg  12374  txbas  12464  blin2  12638  xmettxlem  12715  xmettx  12716  addcncntoplem  12757  mulcncf  12797  logbgcd1irr  13090  logbgcd1irrap  13093
  Copyright terms: Public domain W3C validator