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

Theorem rexlimdv 2482
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 1462 . 2 𝑥𝜑
2 nfv 1462 . 2 𝑥𝜒
3 rexlimdv.1 . 2 (𝜑 → (𝑥𝐴 → (𝜓𝜒)))
41, 2, 3rexlimd 2480 1 (𝜑 → (∃𝑥𝐴 𝜓𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1434  wrex 2354
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441  ax-17 1460  ax-ial 1468  ax-i5r 1469
This theorem depends on definitions:  df-bi 115  df-nf 1391  df-ral 2358  df-rex 2359
This theorem is referenced by:  rexlimdva  2483  rexlimdv3a  2485  rexlimdvw  2486  rexlimdvv  2489  trintssmOLD  3918  ssorduni  4267  funcnvuni  5036  dffo3  5391  smoiun  5998  tfrlem9  6016  ordiso2  6635  axprecex  7318  recexap  8020  zdiv  8730  btwnz  8761  lbzbi  8996
  Copyright terms: Public domain W3C validator