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

Theorem rexlimiva 2484
Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 18-Dec-2006.)
Hypothesis
Ref Expression
rexlimiva.1 ((𝑥𝐴𝜑) → 𝜓)
Assertion
Ref Expression
rexlimiva (∃𝑥𝐴 𝜑𝜓)
Distinct variable group:   𝜓,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝐴(𝑥)

Proof of Theorem rexlimiva
StepHypRef Expression
1 rexlimiva.1 . . 3 ((𝑥𝐴𝜑) → 𝜓)
21ex 113 . 2 (𝑥𝐴 → (𝜑𝜓))
32rexlimiv 2483 1 (∃𝑥𝐴 𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wcel 1438  wrex 2360
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 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445  ax-17 1464  ax-ial 1472  ax-i5r 1473
This theorem depends on definitions:  df-bi 115  df-nf 1395  df-ral 2364  df-rex 2365
This theorem is referenced by:  unon  4328  reg2exmidlema  4350  ssfilem  6591  diffitest  6603  djuun  6760  djuss  6761  updjud  6773  finnum  6811  dmaddpqlem  6936  nqpi  6937  nq0nn  7001  recexprlemm  7183  rexanuz  10421  r19.2uz  10426  maxleast  10646  fsum2dlemstep  10828  fisumcom2  10832  0dvds  11094  even2n  11152  m1expe  11177  m1exp1  11179  bj-nn0suc  11859  bj-nn0sucALT  11873
  Copyright terms: Public domain W3C validator