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

Theorem rexlimdv 2593
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 1528 . 2 𝑥𝜑
2 nfv 1528 . 2 𝑥𝜒
3 rexlimdv.1 . 2 (𝜑 → (𝑥𝐴 → (𝜓𝜒)))
41, 2, 3rexlimd 2591 1 (𝜑 → (∃𝑥𝐴 𝜓𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  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:  rexlimdva  2594  rexlimdv3a  2596  rexlimdva2  2597  rexlimdvw  2598  rexlimdvv  2601  ssorduni  4486  funcnvuni  5285  dffo3  5663  smoiun  6301  tfrlem9  6319  ordiso2  7033  axprecex  7878  recexap  8609  zdiv  9340  btwnz  9371  lbzbi  9615  neibl  13961  metcnp3  13981
  Copyright terms: Public domain W3C validator