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

Theorem simpr 107
Description: Elimination of a conjunct. Theorem *3.27 (Simp) of [WhiteheadRussell] p. 112. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 13-Nov-2012.)
Assertion
Ref Expression
simpr  |-  ( (
ph  /\  ps )  ->  ps )

Proof of Theorem simpr
StepHypRef Expression
1 ax-ia2 104 1  |-  ( (
ph  /\  ps )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101
This theorem was proved from axioms:  ax-ia2 104
This theorem is referenced by:  simpri  110  simprd  111  imp  119  adantld  267  ibar  289  pm3.42  319  pm3.4  320  prth  330  simpl2im  372  sylancom  405  adantll  453  adantrl  455  adantlll  457  adantlrl  459  adantrll  461  adantrrl  463  simpllr  494  simplrr  496  simprlr  498  simprrr  500  anabs7  516  jcab  545  pm4.38  547  pm5.21  621  ioran  679  pm3.14  680  ordi  740  pm4.39  746  pm5.16  748  pm5.54dc  838  intnan  849  intnand  851  dcan  853  bimsc1  881  niabn  885  simp1r  940  simp2r  942  simp3r  944  3anandirs  1254  truanOLD  1277  bilukdc  1303  19.26  1386  exsimpr  1525  19.40  1538  cbvexh  1654  sbequilem  1735  spsbe  1739  cbvexdh  1817  euan  1972  moan  1985  datisi  2026  fresison  2034  rexex  2385  r19.26  2458  r19.40  2481  cbvraldva2  2554  cbvrexdva2  2555  gencbvex  2617  rspct  2666  rspcimdv  2674  rspcimedv  2675  rr19.28v  2706  elrab3t  2720  reu6  2753  rmob  2878  csbiebt  2914  rabssab  3055  ssddif  3199  difin  3202  difrab  3239  preqsn  3574  opprc2  3600  dfnfc2  3626  intmin4  3671  sndisj  3788  exss  3991  euotd  4019  frirrg  4115  suctr  4186  ordtri2or2exmid  4324  wetriext  4329  reg3exmidlemwe  4331  tfisi  4338  peano2  4346  relop  4514  releldm  4597  relelrn  4598  resiexg  4681  trin2  4744  xpmlem  4772  unielrel  4873  relcoi2  4876  iota2df  4919  iota2  4921  funopab4  4965  fun11uni  4997  imadiflem  5006  imain  5009  fneq12  5020  f1ssr  5126  fvelrnb  5249  ssimaex  5262  fvmpt2d  5285  fvmptdf  5286  dffo3  5342  ffvresb  5356  fmptco  5358  funfvima3  5420  f1imass  5441  fliftf  5467  fliftval  5468  riota2df  5516  riota5f  5520  acexmidlemcase  5535  ovprc2  5570  eloprabga  5619  eqfnov2  5636  ovmpt2dxf  5654  fnofval  5749  offval2  5754  ofrfval2  5755  caofinvl  5761  2ndrn  5837  1st2ndbr  5838  cnvf1o  5874  f1o2ndf1  5877  mpt2xopoveq  5886  sprmpt2  5888  dftpos4  5909  tpostpos  5910  tposf12  5915  dfsmo2  5933  smores  5938  tfrlem1  5954  tfrlem3ag  5955  tfrlem3a  5956  tfrlemisucaccv  5970  tfrlemi1  5977  tfrexlem  5979  rdgivallem  5999  frecabex  6015  frectfr  6016  frecrdg  6023  freccl  6024  oawordi  6080  nntri3  6106  nndifsnid  6111  nnaordi  6112  nnaordex  6131  nnawordex  6132  nnm00  6133  ersymb  6151  ertr  6152  erref  6157  iserd  6163  swoer  6165  erth  6181  iinerm  6209  erinxp  6211  ecinxp  6212  qsel  6214  qliftel  6217  qliftfun  6219  dom3  6287  ssdomg  6289  cnven  6319  phplem4dom  6355  phpm  6358  phpelm  6359  fidifsnen  6362  fidifsnid  6363  fin0  6373  fin0or  6374  fientri3  6384  suplubti  6406  supisolem  6412  supisoex  6413  ordiso2  6415  dmaddpqlem  6533  nqpi  6534  mulcanenq  6541  ltaddnq  6563  ltexnqq  6564  prarloclemarch2  6575  ltrnqg  6576  ltnnnq  6579  enq0sym  6588  nqnq0pi  6594  nq0nn  6598  mulcanenq0ec  6601  addnq0mo  6603  mulnq0mo  6604  addnnnq0  6605  prloc  6647  prarloclemlt  6649  prarloclemlo  6650  ltdfpr  6662  genplt2i  6666  genpml  6673  genpmu  6674  addnqprllem  6683  addnqprulem  6684  addnqprl  6685  addnqpru  6686  nqprloc  6701  appdivnq  6719  appdiv0nq  6720  mulnqprl  6724  mulnqpru  6725  distrlem1prl  6738  distrlem1pru  6739  ltprordil  6745  1idprl  6746  1idpru  6747  ltexprlemrl  6766  ltexprlemru  6768  ltexpri  6769  addcanprleml  6770  addcanprlemu  6771  recexprlem1ssl  6789  recexpr  6794  aptiprlemu  6796  archpr  6799  cauappcvgprlemopl  6802  cauappcvgprlemdisj  6807  cauappcvgprlemloc  6808  cauappcvgprlemladdfu  6810  cauappcvgprlemladdfl  6811  cauappcvgprlemladdru  6812  cauappcvgprlemladdrl  6813  caucvgprlemm  6824  caucvgprlemopl  6825  caucvgprlemloc  6831  caucvgprlemladdfu  6833  caucvgprlemladdrl  6834  caucvgprlemlim  6837  caucvgprprlemval  6844  caucvgprprlemml  6850  caucvgprprlemopl  6853  caucvgprprlemopu  6855  caucvgprprlemloc  6859  caucvgprprlemexbt  6862  caucvgprprlemexb  6863  caucvgprprlemaddq  6864  caucvgprprlemlim  6867  addsrmo  6886  mulsrmo  6887  addsrpr  6888  mulsrpr  6889  0idsr  6910  1idsr  6911  recexsrlem  6917  addgt0sr  6918  srpospr  6925  prsradd  6928  prsrlt  6929  caucvgsrlemfv  6933  caucvgsrlemgt1  6937  caucvgsrlemoffval  6938  caucvgsrlemoffcau  6940  caucvgsrlemoffres  6942  rereceu  7021  axarch  7023  nntopi  7026  axcaucvglemval  7029  muladd11r  7230  cnegexlem1  7249  cnegex  7252  negeu  7265  pncan  7280  pncan3  7282  npcan  7283  addid0  7443  mulneg1  7464  lelttrdi  7495  ltnegcon2  7533  add20  7543  subge0  7544  lesub0  7548  reapval  7641  recexre  7643  apreap  7652  ltmul1a  7656  reapneg  7662  cru  7667  apsym  7671  apcotr  7672  apadd1  7673  apneg  7676  mulext1  7677  apti  7687  gt0ap0  7690  ap0gt0  7703  recexap  7708  rerecclap  7781  recgt0  7891  prodgt0gt0  7892  lemul1a  7899  lemul12a  7903  lt2msq  7927  ltrec1  7929  recreclt  7941  creui  7988  cju  7989  avglt2  8221  un0addcl  8272  nn0ge2m1nn  8299  nn0nndivcl  8301  elnn0z  8315  peano2z  8338  elz2  8370  peano5uzti  8405  zindd  8415  eluzadd  8597  nn0pzuz  8626  eluz2b2  8637  eqreznegel  8646  nn0ge2m1nnALT  8650  divfnzn  8653  qmulz  8655  qapne  8671  qreccl  8674  cnref1o  8680  ge0p1rp  8712  xrltso  8818  z2ge  8840  xltnegi  8849  ixxssixx  8872  lincmb01cmp  8972  iccf1o  8973  zltaddlt1le  8975  fztri3or  9005  fzdcel  9006  fznlem  9007  fzn  9008  uzsubsubfz  9013  fzsplit2  9016  fzopth  9026  fzdifsuc  9045  fzrev2i  9050  elfz1b  9054  fzneuz  9065  fzrevral  9069  ige2m1fz  9074  elfz0ubfz0  9084  elfz0fzfz0  9085  4fvwrd4  9099  2ffzeq  9100  fzospliti  9134  fzosplit  9135  fzo1fzo0n0  9141  fzonmapblen  9145  fzoaddel  9150  fzosubel  9152  fzosubel3  9154  elfzodifsumelfzo  9159  elfzom1elp1fzo  9160  elfzom1p1elfzo  9172  elfzonelfzo  9188  peano2fzor  9190  fvinim0ffz  9198  qtri3or  9200  qbtwnzlemstep  9205  rebtwn2zlemstep  9209  qbtwnxr  9214  flqge  9232  flqltnz  9237  flqaddz  9247  btwnzge0  9250  flltdivnn0lt  9254  intfracq  9270  flqdiv  9271  modqid0  9300  q0mod  9305  q1mod  9306  modqmuladdim  9317  modqmuladdnn0  9318  q2txmodxeq0  9334  q2submod  9335  modifeq2int  9336  modqsubdir  9343  modsumfzodifsn  9346  addmodlteq  9348  frec2uzzd  9350  frec2uzuzd  9352  frec2uzrand  9355  frec2uzf1od  9356  frecuzrdgrrn  9358  frec2uzrdg  9359  frecuzrdgfn  9362  frecuzrdgcl  9363  frecuzrdgsuc  9365  frecfzennn  9367  iseqf  9388  iseqss  9390  iseqfeq2  9393  iseqfeq  9395  isermono  9401  iseqsplit  9402  iseqid3s  9410  iseqid  9411  iseqhomo  9412  iseqz  9413  expivallem  9421  expival  9422  expinnval  9423  expp1  9427  rpexpcl  9439  expaddzaplem  9463  leexp1a  9475  exple1  9476  subsq  9525  binom2  9529  binom3  9534  bernneq3  9539  expnbnd  9540  nn0opthd  9590  faclbnd  9609  faclbnd6  9612  facubnd  9613  facavg  9614  bcval  9617  bccmpl  9622  ibcval5  9631  bcpasc  9634  shftfvalg  9647  ovshftex  9648  shftdm  9651  shftfib  9652  shftval  9654  shftval5  9658  shftf  9659  2shfti  9660  crre  9685  rereb  9691  cjreim2  9732  cjap  9734  caucvgrelemrec  9806  caucvgrelemcau  9807  caucvgre  9808  cvg1nlemf  9810  cvg1nlemres  9812  uzin2  9814  rexuz3  9817  recvguniq  9822  sqrt0  9831  resqrexlemdecn  9839  resqrexlemlo  9840  resqrexlemcalc3  9843  resqrexlemnm  9845  resqrexlemcvg  9846  resqrexlemoverl  9848  resqrexlemglsq  9849  resqrexlemga  9850  resqrex  9853  sqrtgt0  9861  absrpclap  9888  absext  9890  absmul  9896  leabs  9901  nn0abscl  9912  ltabs  9914  abslt  9915  absle  9916  abssubap0  9917  abstri  9931  cau3lem  9941  caubnd2  9944  clim  10033  climi2  10040  climconst2  10043  climuni  10045  climmpt  10052  climshftlemg  10054  climres  10055  climcn1  10060  subcn2  10063  cn1lem  10065  climadd  10077  climmul  10078  climsub  10079  climle  10085  climsqz  10086  climsqz2  10087  clim2iser  10088  clim2iser2  10089  iiserex  10090  iisermulc2  10091  iserile  10093  iserige0  10094  climub  10095  climserile  10096  climrecvg1n  10098  climcvg1nlem  10099  serif0  10102  dvdsval2  10111  dvdsdc  10116  moddvds  10117  dvdscmul  10134  dvdsmulc  10135  dvdscmulr  10136  dvdsmulcr  10137  modmulconst  10139  dvdsadd  10150  dvdsadd2b  10154  dvdslelemd  10155  dvdsle  10156  dvdsabseq  10159  dvdseq  10160  divconjdvds  10161  dvds1  10165  fzo0dvdseq  10169  dvdsmod  10174  oddm1even  10186  mod2eq1n2dvds  10191  evennn02n  10194  evennn2n  10195  divalglemnn  10230  divalglemnqt  10232  divalglemeunn  10233  divalglemex  10234  divalglemeuneg  10235  divalg  10236  divalgmod  10239  modremain  10241  sqrt2irr  10251  pw2dvdslemn  10253  pw2dvdseulemle  10255  oddpwdclemxy  10257  oddpwdclemdc  10261  oddpwdc  10262  ialgrp1  10268  ialgcvga  10273  bj-indind  10443  bj-omtrans  10468  qdencn  10511
  Copyright terms: Public domain W3C validator