Theorem simpr 103

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

Step	Hyp	Ref	Expression
1		ax-ia2 100	1 |- ( ( ph /\ ps ) -> ps )

Syntax hints:   -> wi 4   /\ wa 97

This theorem was proved from axioms:  ax-ia2 100

This theorem is referenced by:  simpri  106  simprd  107  imp  115  adantld  263  ibar  285  pm3.42  315  pm3.4  316  prth  326  sylancom  397  adantll  445  adantrl  447  adantlll  449  adantlrl  451  adantrll  453  adantrrl  455  simpllr  486  simplrr  488  simprlr  490  simprrr  492  anabs7  508  jcab  535  pm4.38  537  pm5.21  611  ioran  669  pm3.14  670  ordi  729  pm4.39  735  pm5.16  737  pm5.54dc  827  intnan  838  intnand  840  dcan  842  bimsc1  870  niabn  874  simp1r  929  simp2r  931  simp3r  933  3anandirs  1238  truanOLD  1261  bilukdc  1287  19.26  1370  exsimpr  1509  19.40  1522  cbvexh  1638  sbequilem  1719  spsbe  1723  cbvexdh  1801  euan  1956  moan  1969  datisi  2010  fresison  2018  rexex  2368  r19.26  2441  r19.40  2464  cbvraldva2  2537  cbvrexdva2  2538  gencbvex  2600  rspct  2649  rspcimdv  2657  rspcimedv  2658  rr19.28v  2683  elrab3t  2697  reu6  2730  rmob  2850  csbiebt  2886  rabssab  3027  ssddif  3171  difin  3174  difrab  3211  preqsn  3546  opprc2  3572  dfnfc2  3598  intmin4  3643  sndisj  3760  exss  3963  euotd  3991  frirrg  4087  suctr  4158  ordtri2or2exmid  4296  wetriext  4301  reg3exmidlemwe  4303  tfisi  4310  peano2  4318  relop  4486  releldm  4569  relelrn  4570  resiexg  4653  trin2  4716  xpmlem  4744  unielrel  4845  relcoi2  4848  iota2df  4891  iota2  4893  funopab4  4937  fun11uni  4969  imadiflem  4978  imain  4981  fneq12  4992  f1ssr  5098  fvelrnb  5221  ssimaex  5234  fvmpt2d  5257  fvmptdf  5258  dffo3  5314  ffvresb  5328  fmptco  5330  funfvima3  5392  f1imass  5413  fliftf  5439  fliftval  5440  riota2df  5488  riota5f  5492  acexmidlemcase  5507  ovprc2  5542  eloprabga  5591  eqfnov2  5608  ovmpt2dxf  5626  fnofval  5721  offval2  5726  ofrfval2  5727  caofinvl  5733  2ndrn  5809  1st2ndbr  5810  cnvf1o  5846  f1o2ndf1  5849  mpt2xopoveq  5855  sprmpt2  5857  dftpos4  5878  tpostpos  5879  tposf12  5884  dfsmo2  5902  smores  5907  tfrlem1  5923  tfrlem3ag  5924  tfrlem3a  5925  tfrlemisucaccv  5939  tfrlemi1  5946  tfrexlem  5948  rdgivallem  5968  frecabex  5984  frectfr  5985  frecrdg  5992  freccl  5993  oawordi  6049  nntri3  6075  nndifsnid  6080  nnaordi  6081  nnaordex  6100  nnawordex  6101  nnm00  6102  ersymb  6120  ertr  6121  erref  6126  iserd  6132  swoer  6134  erth  6150  iinerm  6178  erinxp  6180  ecinxp  6181  qsel  6183  qliftel  6186  qliftfun  6188  dom3  6256  ssdomg  6258  cnven  6288  phplem4dom  6324  phpm  6327  phpelm  6328  fidifsnen  6331  fidifsnid  6332  fin0  6342  fin0or  6343  fientri3  6353  ordiso2  6357  dmaddpqlem  6475  nqpi  6476  mulcanenq  6483  ltaddnq  6505  ltexnqq  6506  prarloclemarch2  6517  ltrnqg  6518  ltnnnq  6521  enq0sym  6530  nqnq0pi  6536  nq0nn  6540  mulcanenq0ec  6543  addnq0mo  6545  mulnq0mo  6546  addnnnq0  6547  prloc  6589  prarloclemlt  6591  prarloclemlo  6592  ltdfpr  6604  genplt2i  6608  genpml  6615  genpmu  6616  addnqprllem  6625  addnqprulem  6626  addnqprl  6627  addnqpru  6628  nqprloc  6643  appdivnq  6661  appdiv0nq  6662  mulnqprl  6666  mulnqpru  6667  distrlem1prl  6680  distrlem1pru  6681  ltprordil  6687  1idprl  6688  1idpru  6689  ltexprlemrl  6708  ltexprlemru  6710  ltexpri  6711  addcanprleml  6712  addcanprlemu  6713  recexprlem1ssl  6731  recexpr  6736  aptiprlemu  6738  archpr  6741  cauappcvgprlemopl  6744  cauappcvgprlemdisj  6749  cauappcvgprlemloc  6750  cauappcvgprlemladdfu  6752  cauappcvgprlemladdfl  6753  cauappcvgprlemladdru  6754  cauappcvgprlemladdrl  6755  caucvgprlemm  6766  caucvgprlemopl  6767  caucvgprlemloc  6773  caucvgprlemladdfu  6775  caucvgprlemladdrl  6776  caucvgprlemlim  6779  caucvgprprlemval  6786  caucvgprprlemml  6792  caucvgprprlemopl  6795  caucvgprprlemopu  6797  caucvgprprlemloc  6801  caucvgprprlemexbt  6804  caucvgprprlemexb  6805  caucvgprprlemaddq  6806  caucvgprprlemlim  6809  addsrmo  6828  mulsrmo  6829  addsrpr  6830  mulsrpr  6831  0idsr  6852  1idsr  6853  recexsrlem  6859  addgt0sr  6860  srpospr  6867  prsradd  6870  prsrlt  6871  caucvgsrlemfv  6875  caucvgsrlemgt1  6879  caucvgsrlemoffval  6880  caucvgsrlemoffcau  6882  caucvgsrlemoffres  6884  rereceu  6963  axarch  6965  nntopi  6968  axcaucvglemval  6971  cnegexlem1  7186  cnegex  7189  negeu  7202  pncan  7217  pncan3  7219  npcan  7220  mulneg1  7392  lelttrdi  7421  ltnegcon2  7459  add20  7469  subge0  7470  lesub0  7474  reapval  7567  recexre  7569  apreap  7578  ltmul1a  7582  reapneg  7588  cru  7593  apsym  7597  apcotr  7598  apadd1  7599  apneg  7602  mulext1  7603  apti  7613  gt0ap0  7616  ap0gt0  7629  recexap  7634  rerecclap  7706  recgt0  7816  prodgt0gt0  7817  lemul1a  7824  lemul12a  7828  lt2msq  7852  ltrec1  7854  recreclt  7866  creui  7912  cju  7913  avglt2  8164  un0addcl  8215  nn0ge2m1nn  8242  nn0nndivcl  8244  elnn0z  8258  peano2z  8281  elz2  8312  peano5uzti  8346  zindd  8356  eluzadd  8501  nn0pzuz  8530  eluz2b2  8540  eqreznegel  8549  nn0ge2m1nnALT  8553  divfnzn  8556  qmulz  8558  qapne  8574  qreccl  8576  cnref1o  8582  ge0p1rp  8614  xrltso  8717  z2ge  8739  xltnegi  8748  ixxssixx  8771  lincmb01cmp  8871  iccf1o  8872  fztri3or  8903  fzdcel  8904  fznlem  8905  fzn  8906  uzsubsubfz  8911  fzsplit2  8914  fzopth  8924  fzdifsuc  8943  fzrev2i  8948  elfz1b  8952  fzneuz  8963  fzrevral  8967  ige2m1fz  8972  elfz0ubfz0  8982  elfz0fzfz0  8983  4fvwrd4  8997  2ffzeq  8998  fzospliti  9032  fzosplit  9033  fzo1fzo0n0  9039  fzonmapblen  9043  fzoaddel  9048  fzosubel  9050  fzosubel3  9052  elfzodifsumelfzo  9057  elfzom1elp1fzo  9058  elfzom1p1elfzo  9070  elfzonelfzo  9086  peano2fzor  9088  fvinim0ffz  9096  qtri3or  9098  qbtwnzlemstep  9103  rebtwn2zlemstep  9107  flqge  9124  flqltnz  9129  flqaddz  9139  btwnzge0  9142  flltdivnn0lt  9146  intfracq  9162  flqdiv  9163  frec2uzzd  9186  frec2uzuzd  9188  frec2uzrand  9191  frec2uzf1od  9192  frecuzrdgrrn  9194  frec2uzrdg  9195  frecuzrdgfn  9198  frecuzrdgcl  9199  frecuzrdgsuc  9201  frecfzennn  9203  iseqf  9224  iseqss  9226  iseqfeq2  9229  iseqfeq  9231  isermono  9237  iseqsplit  9238  iseqid3s  9246  iseqid  9247  iseqhomo  9248  expivallem  9256  expival  9257  expinnval  9258  expp1  9262  rpexpcl  9274  expaddzaplem  9298  leexp1a  9309  exple1  9310  subsq  9358  binom2  9362  binom3  9366  bernneq3  9371  expnbnd  9372  shftfvalg  9419  ovshftex  9420  shftdm  9423  shftfib  9424  shftval  9426  shftval5  9430  shftf  9431  2shfti  9432  crre  9457  rereb  9463  cjreim2  9504  cjap  9506  caucvgrelemrec  9578  caucvgrelemcau  9579  caucvgre  9580  cvg1nlemf  9582  cvg1nlemres  9584  uzin2  9586  rexuz3  9588  recvguniq  9593  sqrt0  9602  resqrexlemdecn  9610  resqrexlemlo  9611  resqrexlemcalc3  9614  resqrexlemnm  9616  resqrexlemcvg  9617  resqrexlemoverl  9619  resqrexlemglsq  9620  resqrexlemga  9621  resqrex  9624  sqrtgt0  9632  absrpclap  9659  absext  9661  absmul  9667  leabs  9672  nn0abscl  9681  ltabs  9683  abslt  9684  absle  9685  abssubap0  9686  abstri  9700  cau3lem  9710  caubnd2  9713  clim  9802  climi2  9809  climconst2  9812  climuni  9814  climmpt  9821  climshftlemg  9823  climres  9824  climcn1  9829  subcn2  9832  cn1lem  9834  climadd  9846  climmul  9847  climsub  9848  climle  9854  climsqz  9855  climsqz2  9856  clim2iser  9857  clim2iser2  9858  iiserex  9859  iisermulc2  9860  iserile  9862  iserige0  9863  climub  9864  climserile  9865  climrecvg1n  9867  climcvg1nlem  9868  serif0  9871  sqrt2irr  9878  ialgrp1  9885  ialgcvga  9890  bj-indind  10056  bj-omtrans  10081  qdencn  10124