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

Theorem rexlimddv 2482
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 2479 . 2 (𝜑 → (∃𝑥𝐴 𝜓𝜒))
41, 3mpd 13 1 (𝜑𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wcel 1434  wrex 2350
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 2354  df-rex 2355
This theorem is referenced by:  grprinvlem  5726  grpridd  5728  tfrlemisucaccv  5974  tfrexlem  5983  tfr1onlemsucaccv  5990  tfrcllemsucaccv  6003  fict  6403  fidceq  6404  php5fin  6416  fisbth  6417  fin0  6419  fin0or  6420  diffisn  6427  infnfi  6429  fientri3  6435  unsnfi  6439  unsnfidcex  6440  unsnfidcel  6441  prarloclemarch2  6671  addlocpr  6788  nqprl  6803  nqpru  6804  appdiv0nq  6816  prmuloc  6818  mullocpr  6823  ltprordil  6841  ltaddpr  6849  ltexprlemopl  6853  ltexprlemopu  6855  ltexprlemloc  6859  ltexprlemrl  6862  ltexprlemru  6864  addcanprleml  6866  addcanprlemu  6867  ltaprlem  6870  ltaprg  6871  prplnqu  6872  recexprlemloc  6883  recexprlem1ssl  6885  recexprlem1ssu  6886  aptiprleml  6891  aptiprlemu  6892  ltmprr  6894  archpr  6895  cauappcvgprlemopl  6898  cauappcvgprlemopu  6900  cauappcvgprlemloc  6904  cauappcvgprlem1  6911  cauappcvgprlem2  6912  archrecpr  6916  caucvgprlemopl  6921  caucvgprlemopu  6923  caucvgprlemloc  6927  caucvgprlem2  6932  caucvgprprlemml  6946  caucvgprprlemmu  6947  caucvgprprlemopl  6949  caucvgprprlemopu  6951  caucvgprprlemloc  6955  caucvgprprlemexbt  6958  caucvgprprlem2  6962  prsrriota  7026  caucvgsrlemgt1  7033  caucvgsrlemoffres  7038  rereceu  7117  recriota  7118  axarch  7119  axcaucvglemres  7127  readdcan  7315  cnegex  7353  addcan  7355  addcan2  7356  negeu  7366  ltadd2  7590  recexre  7745  rimul  7752  ltmul1  7759  mulap0  7811  mulcanapd  7818  suprzclex  8526  qbtwnre  9343  sizecl  9805  sizeen  9808  sizedom  9827  sizeunlem  9828  sizeun  9829  cvg1nlemres  10009  cvg1n  10010  recvguniq  10019  resqrexlemoverl  10045  resqrexlemex  10049  fimaxre2  10247  climge0  10301  climrecvg1n  10323  oexpneg  10421  zsupcllemex  10486  zssinfcl  10488  bezoutlemnewy  10529  bezoutlemstep  10530  dfgcd3  10543  bezout  10544  qdencn  10943
  Copyright terms: Public domain W3C validator