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

Theorem rexlimdv 2432
 Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 14-Nov-2002.) (Proof shortened by Eric Schmidt, 22-Dec-2006.)
Hypothesis
Ref Expression
rexlimdv.1 (𝜑 → (𝑥𝐴 → (𝜓𝜒)))
Assertion
Ref Expression
rexlimdv (𝜑 → (∃𝑥𝐴 𝜓𝜒))
Distinct variable groups:   𝜑,𝑥   𝜒,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem rexlimdv
StepHypRef Expression
1 nfv 1421 . 2 𝑥𝜑
2 nfv 1421 . 2 𝑥𝜒
3 rexlimdv.1 . 2 (𝜑 → (𝑥𝐴 → (𝜓𝜒)))
41, 2, 3rexlimd 2430 1 (𝜑 → (∃𝑥𝐴 𝜓𝜒))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∈ wcel 1393  ∃wrex 2307 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427  ax-i5r 1428 This theorem depends on definitions:  df-bi 110  df-nf 1350  df-ral 2311  df-rex 2312 This theorem is referenced by:  rexlimdva  2433  rexlimdv3a  2435  rexlimdvw  2436  rexlimdvv  2439  trintssm  3870  ssorduni  4213  funcnvuni  4968  dffo3  5314  smoiun  5916  tfrlem9  5935  ordiso2  6357  axprecex  6954  recexap  7634  zdiv  8328  btwnz  8357  lbzbi  8551
 Copyright terms: Public domain W3C validator