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

Theorem rexlimddv 2554
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 2550 . 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 103    e. wcel 1480   E.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  7063  exmidfodomrlemrALT  7064  cc2lem  7086  prarloclemarch2  7239  addlocpr  7356  nqprl  7371  nqpru  7372  appdiv0nq  7384  prmuloc  7386  mullocpr  7391  ltprordil  7409  ltaddpr  7417  ltexprlemopl  7421  ltexprlemopu  7423  ltexprlemloc  7427  ltexprlemrl  7430  ltexprlemru  7432  addcanprleml  7434  addcanprlemu  7435  ltaprlem  7438  ltaprg  7439  prplnqu  7440  recexprlemloc  7451  recexprlem1ssl  7453  recexprlem1ssu  7454  aptiprleml  7459  aptiprlemu  7460  ltmprr  7462  archpr  7463  cauappcvgprlemopl  7466  cauappcvgprlemopu  7468  cauappcvgprlemloc  7472  cauappcvgprlem1  7479  cauappcvgprlem2  7480  archrecpr  7484  caucvgprlemopl  7489  caucvgprlemopu  7491  caucvgprlemloc  7495  caucvgprlem2  7500  caucvgprprlemml  7514  caucvgprprlemmu  7515  caucvgprprlemopl  7517  caucvgprprlemopu  7519  caucvgprprlemloc  7523  caucvgprprlemexbt  7526  caucvgprprlem2  7530  suplocexprlemrl  7537  suplocexprlemmu  7538  suplocexprlemru  7539  suplocexprlemdisj  7540  suplocexprlemloc  7541  suplocexprlemex  7542  suplocexprlemub  7543  suplocexprlemlub  7544  prsrriota  7608  caucvgsrlemgt1  7615  caucvgsrlemoffres  7620  suplocsrlem  7628  rereceu  7709  recriota  7710  axarch  7711  axcaucvglemres  7719  axpre-suploclemres  7721  readdcan  7914  cnegex  7952  addcan  7954  addcan2  7955  negeu  7965  ltadd2  8193  recexre  8352  rimul  8359  ltmul1  8366  mulap0  8427  mulcanapd  8434  suprzclex  9161  qbtwnre  10046  hashcl  10539  hashen  10542  fihashdom  10561  hashunlem  10562  hashun  10563  zfz1iso  10596  cvg1nlemres  10769  cvg1n  10770  recvguniq  10779  resqrexlemoverl  10805  resqrexlemex  10809  fimaxre2  11010  climge0  11106  climrecvg1n  11129  fsum3cvg3  11177  expcnvre  11284  mertenslemub  11315  efcllem  11377  oexpneg  11585  zsupcllemex  11650  zssinfcl  11652  bezoutlemnewy  11695  bezoutlemstep  11696  dfgcd3  11709  bezout  11710  ennnfonelemex  11938  ennnfonelemrnh  11940  ennnfonelemf1  11942  ennnfonelemrn  11943  ennnfonelemdm  11944  ennnfonelemnn0  11946  ctinfomlemom  11951  ctinf  11954  ctiunctlemfo  11963  restbasg  12351  cnpnei  12402  cnptopco  12405  xmettx  12693  metcnpi3  12700  mulcncf  12774  dedekindeulemuub  12778  dedekindeulemub  12779  dedekindeulemlu  12782  dedekindicclemuub  12787  dedekindicclemub  12788  dedekindicclemlu  12791  dedekindicc  12794  ivthinclemlopn  12797  ivthinclemuopn  12799  limcimolemlt  12816  limcimo  12817  limccnp2cntop  12829  reeff1oleme  12876  eflt  12879  qdencn  13283  trilpolemlt1  13295
  Copyright terms: Public domain W3C validator