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

Theorem rexlimddv 2554
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 2550 . 2 (𝜑 → (∃𝑥𝐴 𝜓𝜒))
41, 3mpd 13 1 (𝜑𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wcel 1480  wrex 2417
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-i5r 1515
This theorem depends on definitions:  df-bi 116  df-nf 1437  df-ral 2421  df-rex 2422
This theorem is referenced by:  disjiun  3924  nnsucpred  4530  grprinvlem  5965  grpridd  5967  tfrlemisucaccv  6222  tfrexlem  6231  tfr1onlemsucaccv  6238  tfrcllemsucaccv  6251  fict  6762  fidceq  6763  dif1enen  6774  php5fin  6776  fisbth  6777  fin0  6779  fin0or  6780  diffisn  6787  infnfi  6789  fientri3  6803  unsnfi  6807  unsnfidcex  6808  unsnfidcel  6809  fiuni  6866  ctmlemr  6993  ctssdccl  6996  fodjum  7018  fodju0  7019  exmidfodomrlemr  7058  exmidfodomrlemrALT  7059  cc2lem  7081  prarloclemarch2  7234  addlocpr  7351  nqprl  7366  nqpru  7367  appdiv0nq  7379  prmuloc  7381  mullocpr  7386  ltprordil  7404  ltaddpr  7412  ltexprlemopl  7416  ltexprlemopu  7418  ltexprlemloc  7422  ltexprlemrl  7425  ltexprlemru  7427  addcanprleml  7429  addcanprlemu  7430  ltaprlem  7433  ltaprg  7434  prplnqu  7435  recexprlemloc  7446  recexprlem1ssl  7448  recexprlem1ssu  7449  aptiprleml  7454  aptiprlemu  7455  ltmprr  7457  archpr  7458  cauappcvgprlemopl  7461  cauappcvgprlemopu  7463  cauappcvgprlemloc  7467  cauappcvgprlem1  7474  cauappcvgprlem2  7475  archrecpr  7479  caucvgprlemopl  7484  caucvgprlemopu  7486  caucvgprlemloc  7490  caucvgprlem2  7495  caucvgprprlemml  7509  caucvgprprlemmu  7510  caucvgprprlemopl  7512  caucvgprprlemopu  7514  caucvgprprlemloc  7518  caucvgprprlemexbt  7521  caucvgprprlem2  7525  suplocexprlemrl  7532  suplocexprlemmu  7533  suplocexprlemru  7534  suplocexprlemdisj  7535  suplocexprlemloc  7536  suplocexprlemex  7537  suplocexprlemub  7538  suplocexprlemlub  7539  prsrriota  7603  caucvgsrlemgt1  7610  caucvgsrlemoffres  7615  suplocsrlem  7623  rereceu  7704  recriota  7705  axarch  7706  axcaucvglemres  7714  axpre-suploclemres  7716  readdcan  7909  cnegex  7947  addcan  7949  addcan2  7950  negeu  7960  ltadd2  8188  recexre  8347  rimul  8354  ltmul1  8361  mulap0  8422  mulcanapd  8429  suprzclex  9156  qbtwnre  10041  hashcl  10534  hashen  10537  fihashdom  10556  hashunlem  10557  hashun  10558  zfz1iso  10591  cvg1nlemres  10764  cvg1n  10765  recvguniq  10774  resqrexlemoverl  10800  resqrexlemex  10804  fimaxre2  11005  climge0  11101  climrecvg1n  11124  fsum3cvg3  11172  expcnvre  11279  mertenslemub  11310  efcllem  11372  oexpneg  11580  zsupcllemex  11645  zssinfcl  11647  bezoutlemnewy  11690  bezoutlemstep  11691  dfgcd3  11704  bezout  11705  ennnfonelemex  11933  ennnfonelemrnh  11935  ennnfonelemf1  11937  ennnfonelemrn  11938  ennnfonelemdm  11939  ennnfonelemnn0  11941  ctinfomlemom  11946  ctinf  11949  ctiunctlemfo  11958  restbasg  12346  cnpnei  12397  cnptopco  12400  xmettx  12688  metcnpi3  12695  mulcncf  12769  dedekindeulemuub  12773  dedekindeulemub  12774  dedekindeulemlu  12777  dedekindicclemuub  12782  dedekindicclemub  12783  dedekindicclemlu  12786  dedekindicc  12789  ivthinclemlopn  12792  ivthinclemuopn  12794  limcimolemlt  12811  limcimo  12812  limccnp2cntop  12824  reeff1oleme  12870  eflt  12873  qdencn  13275  trilpolemlt1  13287
  Copyright terms: Public domain W3C validator