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

Theorem rexlimddv 2489
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 2486 . 2 (𝜑 → (∃𝑥𝐴 𝜓𝜒))
41, 3mpd 13 1 (𝜑𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wcel 1436  wrex 2356
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 1379  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-4 1443  ax-17 1462  ax-ial 1470  ax-i5r 1471
This theorem depends on definitions:  df-bi 115  df-nf 1393  df-ral 2360  df-rex 2361
This theorem is referenced by:  grprinvlem  5796  grpridd  5798  tfrlemisucaccv  6044  tfrexlem  6053  tfr1onlemsucaccv  6060  tfrcllemsucaccv  6073  fict  6536  fidceq  6537  dif1enen  6548  php5fin  6550  fisbth  6551  fin0  6553  fin0or  6554  diffisn  6561  infnfi  6563  fientri3  6577  unsnfi  6581  unsnfidcex  6582  unsnfidcel  6583  fodjuomnilemm  6745  fodjuomnilem0  6746  exmidfodomrlemr  6772  exmidfodomrlemrALT  6773  prarloclemarch2  6922  addlocpr  7039  nqprl  7054  nqpru  7055  appdiv0nq  7067  prmuloc  7069  mullocpr  7074  ltprordil  7092  ltaddpr  7100  ltexprlemopl  7104  ltexprlemopu  7106  ltexprlemloc  7110  ltexprlemrl  7113  ltexprlemru  7115  addcanprleml  7117  addcanprlemu  7118  ltaprlem  7121  ltaprg  7122  prplnqu  7123  recexprlemloc  7134  recexprlem1ssl  7136  recexprlem1ssu  7137  aptiprleml  7142  aptiprlemu  7143  ltmprr  7145  archpr  7146  cauappcvgprlemopl  7149  cauappcvgprlemopu  7151  cauappcvgprlemloc  7155  cauappcvgprlem1  7162  cauappcvgprlem2  7163  archrecpr  7167  caucvgprlemopl  7172  caucvgprlemopu  7174  caucvgprlemloc  7178  caucvgprlem2  7183  caucvgprprlemml  7197  caucvgprprlemmu  7198  caucvgprprlemopl  7200  caucvgprprlemopu  7202  caucvgprprlemloc  7206  caucvgprprlemexbt  7209  caucvgprprlem2  7213  prsrriota  7277  caucvgsrlemgt1  7284  caucvgsrlemoffres  7289  rereceu  7368  recriota  7369  axarch  7370  axcaucvglemres  7378  readdcan  7566  cnegex  7604  addcan  7606  addcan2  7607  negeu  7617  ltadd2  7841  recexre  7996  rimul  8003  ltmul1  8010  mulap0  8062  mulcanapd  8069  suprzclex  8777  qbtwnre  9596  hashcl  10086  hashen  10089  fihashdom  10108  hashunlem  10109  hashun  10110  zfz1iso  10143  cvg1nlemres  10314  cvg1n  10315  recvguniq  10324  resqrexlemoverl  10350  resqrexlemex  10354  fimaxre2  10553  climge0  10607  climrecvg1n  10629  fisumcvg3  10676  oexpneg  10759  zsupcllemex  10824  zssinfcl  10826  bezoutlemnewy  10867  bezoutlemstep  10868  dfgcd3  10881  bezout  10882  nnsucpred  11336  qdencn  11360
  Copyright terms: Public domain W3C validator