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

Theorem rexlimiva 2518
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 2517 1 (∃𝑥𝐴 𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wcel 1463  wrex 2391
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-4 1470  ax-17 1489  ax-ial 1497  ax-i5r 1498
This theorem depends on definitions:  df-bi 116  df-nf 1420  df-ral 2395  df-rex 2396
This theorem is referenced by:  unon  4387  reg2exmidlema  4409  ssfilem  6722  diffitest  6734  fival  6810  elfi2  6812  fi0  6815  djuss  6907  updjud  6919  enumct  6952  finnum  6989  dmaddpqlem  7133  nqpi  7134  nq0nn  7198  recexprlemm  7380  rexanuz  10652  r19.2uz  10657  maxleast  10877  fsum2dlemstep  11095  fisumcom2  11099  0dvds  11361  even2n  11419  m1expe  11444  m1exp1  11446  epttop  12102  neipsm  12166  tgioo  12532  bj-nn0suc  12854  bj-nn0sucALT  12868
  Copyright terms: Public domain W3C validator