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

Theorem rexlimdv 2586
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 1521 . 2 𝑥𝜑
2 nfv 1521 . 2 𝑥𝜒
3 rexlimdv.1 . 2 (𝜑 → (𝑥𝐴 → (𝜓𝜒)))
41, 2, 3rexlimd 2584 1 (𝜑 → (∃𝑥𝐴 𝜓𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 2141  wrex 2449
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 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-i5r 1528
This theorem depends on definitions:  df-bi 116  df-nf 1454  df-ral 2453  df-rex 2454
This theorem is referenced by:  rexlimdva  2587  rexlimdv3a  2589  rexlimdva2  2590  rexlimdvw  2591  rexlimdvv  2594  ssorduni  4471  funcnvuni  5267  dffo3  5643  smoiun  6280  tfrlem9  6298  ordiso2  7012  axprecex  7842  recexap  8571  zdiv  9300  btwnz  9331  lbzbi  9575  neibl  13285  metcnp3  13305
  Copyright terms: Public domain W3C validator