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

Theorem rexlimdv 2449
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 1437 . 2 𝑥𝜑
2 nfv 1437 . 2 𝑥𝜒
3 rexlimdv.1 . 2 (𝜑 → (𝑥𝐴 → (𝜓𝜒)))
41, 2, 3rexlimd 2447 1 (𝜑 → (∃𝑥𝐴 𝜓𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  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:  rexlimdva  2450  rexlimdv3a  2452  rexlimdvw  2453  rexlimdvv  2456  trintssmOLD  3898  ssorduni  4240  funcnvuni  4995  dffo3  5341  smoiun  5946  tfrlem9  5965  ordiso2  6414  axprecex  7011  recexap  7707  zdiv  8385  btwnz  8415  lbzbi  8647
  Copyright terms: Public domain W3C validator