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

Theorem rexlimiva 2445
 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 112 . 2 (𝑥𝐴 → (𝜑𝜓))
32rexlimiv 2444 1 (∃𝑥𝐴 𝜑𝜓)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 101   ∈ wcel 1409  ∃wrex 2324 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-4 1416  ax-17 1435  ax-ial 1443  ax-i5r 1444 This theorem depends on definitions:  df-bi 114  df-nf 1366  df-ral 2328  df-rex 2329 This theorem is referenced by:  unon  4265  reg2exmidlema  4287  ssfiexmid  6367  diffitest  6375  finnum  6421  dmaddpqlem  6533  nqpi  6534  nq0nn  6598  recexprlemm  6780  rexanuz  9815  r19.2uz  9820  0dvds  10128  even2n  10185  m1expe  10211  m1exp1  10213  bj-nn0suc  10476  bj-nn0sucALT  10490
 Copyright terms: Public domain W3C validator