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

Theorem rexlimddv 2437
Description: Restricted existential elimination rule of natural deduction. (Contributed by Mario Carneiro, 15-Jun-2016.)
Hypotheses
Ref Expression
rexlimddv.1 (𝜑 → ∃𝑥𝐴 𝜓)
rexlimddv.2 ((𝜑 ∧ (𝑥𝐴𝜓)) → 𝜒)
Assertion
Ref Expression
rexlimddv (𝜑𝜒)
Distinct variable groups:   𝜑,𝑥   𝜒,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem rexlimddv
StepHypRef Expression
1 rexlimddv.1 . 2 (𝜑 → ∃𝑥𝐴 𝜓)
2 rexlimddv.2 . . 3 ((𝜑 ∧ (𝑥𝐴𝜓)) → 𝜒)
32rexlimdvaa 2434 . 2 (𝜑 → (∃𝑥𝐴 𝜓𝜒))
41, 3mpd 13 1 (𝜑𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 97  wcel 1393  wrex 2307
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427  ax-i5r 1428
This theorem depends on definitions:  df-bi 110  df-nf 1350  df-ral 2311  df-rex 2312
This theorem is referenced by:  grprinvlem  5695  grpridd  5697  tfrlemisucaccv  5939  tfrexlem  5948  fidceq  6330  php5fin  6339  fisbth  6340  fin0  6342  fin0or  6343  diffisn  6350  fientri3  6353  prarloclemarch2  6517  addlocpr  6634  nqprl  6649  nqpru  6650  appdiv0nq  6662  prmuloc  6664  mullocpr  6669  ltprordil  6687  ltaddpr  6695  ltexprlemopl  6699  ltexprlemopu  6701  ltexprlemloc  6705  ltexprlemrl  6708  ltexprlemru  6710  addcanprleml  6712  addcanprlemu  6713  ltaprlem  6716  ltaprg  6717  prplnqu  6718  recexprlemloc  6729  recexprlem1ssl  6731  recexprlem1ssu  6732  aptiprleml  6737  aptiprlemu  6738  ltmprr  6740  archpr  6741  cauappcvgprlemopl  6744  cauappcvgprlemopu  6746  cauappcvgprlemloc  6750  cauappcvgprlem1  6757  cauappcvgprlem2  6758  archrecpr  6762  caucvgprlemopl  6767  caucvgprlemopu  6769  caucvgprlemloc  6773  caucvgprlem2  6778  caucvgprprlemml  6792  caucvgprprlemmu  6793  caucvgprprlemopl  6795  caucvgprprlemopu  6797  caucvgprprlemloc  6801  caucvgprprlemexbt  6804  caucvgprprlem2  6808  prsrriota  6872  caucvgsrlemgt1  6879  caucvgsrlemoffres  6884  rereceu  6963  recriota  6964  axarch  6965  axcaucvglemres  6973  readdcan  7153  cnegex  7189  addcan  7191  addcan2  7192  negeu  7202  ltadd2  7416  recexre  7569  rimul  7576  ltmul1  7583  mulap0  7635  mulcanapd  7642  qbtwnre  9111  cvg1nlemres  9584  cvg1n  9585  recvguniq  9593  resqrexlemoverl  9619  resqrexlemex  9623  climge0  9845  climrecvg1n  9867  qdencn  10123
  Copyright terms: Public domain W3C validator