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

Theorem rexlimdvva 2489
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 113 . 2 (𝜑 → ((𝑥𝐴𝑦𝐵) → (𝜓𝜒)))
32rexlimdvv 2488 1 (𝜑 → (∃𝑥𝐴𝑦𝐵 𝜓𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wcel 1434  wrex 2354
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441  ax-17 1460  ax-ial 1468  ax-i5r 1469
This theorem depends on definitions:  df-bi 115  df-nf 1391  df-ral 2358  df-rex 2359
This theorem is referenced by:  ovelrn  5700  f1o2ndf1  5900  eroveu  6284  eroprf  6286  genipv  6796  genpelvl  6799  genpelvu  6800  genprndl  6808  genprndu  6809  addlocpr  6823  addnqprlemrl  6844  addnqprlemru  6845  mulnqprlemrl  6860  mulnqprlemru  6861  ltsopr  6883  ltaddpr  6884  ltexprlemfl  6896  ltexprlemrl  6897  ltexprlemfu  6898  ltexprlemru  6899  cauappcvgprlemladdfu  6941  cauappcvgprlemladdfl  6942  caucvgprlemdisj  6961  caucvgprlemladdfu  6964  caucvgprprlemdisj  6989  apreap  7789  apreim  7805  apirr  7807  apsym  7808  apcotr  7809  apadd1  7810  apneg  7813  mulext1  7814  apti  7824  qapne  8840  qtri3or  9364  exbtwnzlemex  9371  rebtwn2z  9376  cjap  9977  rexanre  10290  climcn2  10332  dvds2lem  10398  bezoutlemnewy  10575  bezoutlembi  10584  dvdsmulgcd  10604  divgcdcoprm0  10673  cncongr1  10675  sqrt2irrap  10748
  Copyright terms: Public domain W3C validator