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

Theorem rexlimiva 2589
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 115 . 2 (𝑥𝐴 → (𝜑𝜓))
32rexlimiv 2588 1 (∃𝑥𝐴 𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wcel 2148  wrex 2456
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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-i5r 1535
This theorem depends on definitions:  df-bi 117  df-nf 1461  df-ral 2460  df-rex 2461
This theorem is referenced by:  unon  4512  reg2exmidlema  4535  ssfilem  6877  diffitest  6889  fival  6971  elfi2  6973  fi0  6976  djuss  7071  updjud  7083  enumct  7116  finnum  7184  dmaddpqlem  7378  nqpi  7379  nq0nn  7443  recexprlemm  7625  rexanuz  10999  r19.2uz  11004  maxleast  11224  fsum2dlemstep  11444  fisumcom2  11448  fprod2dlemstep  11632  fprodcom2fi  11636  0dvds  11820  even2n  11881  m1expe  11906  m1exp1  11908  modprm0  12256  dfgrp2  12907  epttop  13675  neipsm  13739  tgioo  14131  sin0pilem2  14288  pilem3  14289  bj-nn0suc  14801  bj-nn0sucALT  14815  trirec0xor  14878
  Copyright terms: Public domain W3C validator