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

Theorem rexlimiva 2548
 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 114 . 2 (𝑥𝐴 → (𝜑𝜓))
32rexlimiv 2547 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:  unon  4437  reg2exmidlema  4459  ssfilem  6780  diffitest  6792  fival  6874  elfi2  6876  fi0  6879  djuss  6971  updjud  6983  enumct  7016  finnum  7066  dmaddpqlem  7236  nqpi  7237  nq0nn  7301  recexprlemm  7483  rexanuz  10819  r19.2uz  10824  maxleast  11044  fsum2dlemstep  11262  fisumcom2  11266  0dvds  11583  even2n  11641  m1expe  11666  m1exp1  11668  epttop  12332  neipsm  12396  tgioo  12788  sin0pilem2  12945  pilem3  12946  bj-nn0suc  13377  bj-nn0sucALT  13391  trirec0xor  13458
 Copyright terms: Public domain W3C validator