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

Theorem rexlimddv 2597
Description: Restricted existential elimination rule of natural deduction. (Contributed by Mario Carneiro, 15-Jun-2016.)
Hypotheses
Ref Expression
rexlimddv.1  |-  ( ph  ->  E. x  e.  A  ps )
rexlimddv.2  |-  ( (
ph  /\  ( x  e.  A  /\  ps )
)  ->  ch )
Assertion
Ref Expression
rexlimddv  |-  ( ph  ->  ch )
Distinct variable groups:    ph, x    ch, x
Allowed substitution hints:    ps( x)    A( x)

Proof of Theorem rexlimddv
StepHypRef Expression
1 rexlimddv.1 . 2  |-  ( ph  ->  E. x  e.  A  ps )
2 rexlimddv.2 . . 3  |-  ( (
ph  /\  ( x  e.  A  /\  ps )
)  ->  ch )
32rexlimdvaa 2593 . 2  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
41, 3mpd 13 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    e. wcel 2146   E.wrex 2454
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1445  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-4 1508  ax-17 1524  ax-ial 1532  ax-i5r 1533
This theorem depends on definitions:  df-bi 117  df-nf 1459  df-ral 2458  df-rex 2459
This theorem is referenced by:  disjiun  3993  nnsucpred  4610  tfrlemisucaccv  6316  tfrexlem  6325  tfr1onlemsucaccv  6332  tfrcllemsucaccv  6345  fict  6858  fidceq  6859  dif1enen  6870  php5fin  6872  fisbth  6873  fin0  6875  fin0or  6876  diffisn  6883  infnfi  6885  fientri3  6904  unsnfi  6908  unsnfidcex  6909  unsnfidcel  6910  fiuni  6967  ctmlemr  7097  ctssdccl  7100  fodjum  7134  fodju0  7135  exmidfodomrlemr  7191  exmidfodomrlemrALT  7192  cc2lem  7240  prarloclemarch2  7393  addlocpr  7510  nqprl  7525  nqpru  7526  appdiv0nq  7538  prmuloc  7540  mullocpr  7545  ltprordil  7563  ltaddpr  7571  ltexprlemopl  7575  ltexprlemopu  7577  ltexprlemloc  7581  ltexprlemrl  7584  ltexprlemru  7586  addcanprleml  7588  addcanprlemu  7589  ltaprlem  7592  ltaprg  7593  prplnqu  7594  recexprlemloc  7605  recexprlem1ssl  7607  recexprlem1ssu  7608  aptiprleml  7613  aptiprlemu  7614  ltmprr  7616  archpr  7617  cauappcvgprlemopl  7620  cauappcvgprlemopu  7622  cauappcvgprlemloc  7626  cauappcvgprlem1  7633  cauappcvgprlem2  7634  archrecpr  7638  caucvgprlemopl  7643  caucvgprlemopu  7645  caucvgprlemloc  7649  caucvgprlem2  7654  caucvgprprlemml  7668  caucvgprprlemmu  7669  caucvgprprlemopl  7671  caucvgprprlemopu  7673  caucvgprprlemloc  7677  caucvgprprlemexbt  7680  caucvgprprlem2  7684  suplocexprlemrl  7691  suplocexprlemmu  7692  suplocexprlemru  7693  suplocexprlemdisj  7694  suplocexprlemloc  7695  suplocexprlemex  7696  suplocexprlemub  7697  suplocexprlemlub  7698  prsrriota  7762  caucvgsrlemgt1  7769  caucvgsrlemoffres  7774  suplocsrlem  7782  rereceu  7863  recriota  7864  axarch  7865  axcaucvglemres  7873  axpre-suploclemres  7875  readdcan  8071  cnegex  8109  addcan  8111  addcan2  8112  negeu  8122  ltadd2  8350  recexre  8509  rimul  8516  ltmul1  8523  mulap0  8584  mulcanapd  8591  suprzclex  9322  qbtwnre  10225  hashcl  10727  hashen  10730  fihashdom  10750  hashunlem  10751  hashun  10752  zfz1iso  10788  cvg1nlemres  10961  cvg1n  10962  recvguniq  10971  resqrexlemoverl  10997  resqrexlemex  11001  fimaxre2  11202  climge0  11300  climrecvg1n  11323  fsum3cvg3  11371  expcnvre  11478  mertenslemub  11509  efcllem  11634  oexpneg  11848  zsupcllemex  11913  zssinfcl  11915  suprzubdc  11919  zsupssdc  11921  suprzcl2dc  11922  bezoutlemnewy  11963  bezoutlemstep  11964  dfgcd3  11977  bezout  11978  isprm5lem  12107  ennnfonelemex  12381  ennnfonelemrnh  12383  ennnfonelemf1  12385  ennnfonelemrn  12386  ennnfonelemdm  12387  ennnfonelemnn0  12389  ctinfomlemom  12394  ctinf  12397  ctiunctlemfo  12406  nninfdclemcl  12415  nninfdc  12420  grprinvlem  12669  grpridd  12671  grprcan  12770  restbasg  13161  cnpnei  13212  cnptopco  13215  xmettx  13503  metcnpi3  13510  mulcncf  13584  dedekindeulemuub  13588  dedekindeulemub  13589  dedekindeulemlu  13592  dedekindicclemuub  13597  dedekindicclemub  13598  dedekindicclemlu  13601  dedekindicc  13604  ivthinclemlopn  13607  ivthinclemuopn  13609  limcimolemlt  13626  limcimo  13627  limccnp2cntop  13639  reeff1oleme  13686  eflt  13689  bj-charfunr  14044  qdencn  14258  trilpolemlt1  14272  nconstwlpolemgt0  14294
  Copyright terms: Public domain W3C validator