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

Theorem rexlimdv 2525
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 1493 . 2 𝑥𝜑
2 nfv 1493 . 2 𝑥𝜒
3 rexlimdv.1 . 2 (𝜑 → (𝑥𝐴 → (𝜓𝜒)))
41, 2, 3rexlimd 2523 1 (𝜑 → (∃𝑥𝐴 𝜓𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1465  wrex 2394
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 1408  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-4 1472  ax-17 1491  ax-ial 1499  ax-i5r 1500
This theorem depends on definitions:  df-bi 116  df-nf 1422  df-ral 2398  df-rex 2399
This theorem is referenced by:  rexlimdva  2526  rexlimdv3a  2528  rexlimdva2  2529  rexlimdvw  2530  rexlimdvv  2533  ssorduni  4373  funcnvuni  5162  dffo3  5535  smoiun  6166  tfrlem9  6184  ordiso2  6888  axprecex  7656  recexap  8382  zdiv  9107  btwnz  9138  lbzbi  9376  neibl  12587  metcnp3  12607
  Copyright terms: Public domain W3C validator