Theorem simpr 108

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 105	1 |- ( ( ph /\ ps ) -> ps )

Syntax hints:   -> wi 4   /\ wa 102

This theorem was proved from axioms:  ax-ia2 105

This theorem is referenced by:  simpri  111  simprd  112  imp  122  adantld  272  ibar  295  pm3.42  325  pm3.4  326  prth  336  simpl2im  378  sylancom  411  adantll  459  adantrl  461  adantlll  463  adantlrl  465  adantrll  467  adantrrl  469  simpllr  500  simplrr  502  simprlr  504  simprrr  506  anabs7  538  jcab  567  pm4.38  569  pm5.21  643  ioran  701  pm3.14  702  ordi  762  pm4.39  768  pm5.16  770  pm5.54dc  860  intnan  871  intnand  873  dcan  875  bimsc1  904  niabn  908  simp1r  963  simp2r  965  simp3r  967  3anandirs  1279  bilukdc  1327  19.26  1410  exsimpr  1549  19.40  1562  cbvexh  1678  sbequilem  1759  spsbe  1763  cbvexdh  1842  euan  1997  moan  2010  datisi  2051  fresison  2059  rexex  2410  r19.26  2485  r19.40  2508  cbvraldva2  2581  cbvrexdva2  2582  gencbvex  2645  rspct  2694  rspcimdv  2702  rspcimedv  2703  rr19.28v  2734  elrab3t  2748  reu6  2781  rmob  2906  csbiebt  2942  rabssab  3081  ssddif  3198  difin  3201  difrab  3238  preqsn  3567  opprc2  3593  dfnfc2  3619  intmin4  3664  sndisj  3781  exss  3982  euotd  4009  frirrg  4105  suctr  4176  ordtri2or2exmid  4314  wetriext  4319  reg3exmidlemwe  4321  tfisi  4328  peano2  4336  relop  4504  releldm  4587  relelrn  4588  resiexg  4673  trin2  4736  xpmlem  4764  unielrel  4865  relcoi2  4868  iota2df  4911  iota2  4913  funopab4  4957  fun11uni  4989  imadiflem  4998  imain  5001  fneq12  5012  f1ssr  5118  fvelrnb  5242  ssimaex  5255  fvmpt2d  5278  fvmptdf  5279  dffo3  5335  ffvresb  5349  fmptco  5351  funfvima3  5413  f1imass  5434  fliftf  5459  fliftval  5460  riota2df  5508  riota5f  5512  acexmidlemcase  5527  ovprc2  5562  eloprabga  5611  eqfnov2  5628  ovmpt2dxf  5646  fnofval  5741  offval2  5746  ofrfval2  5747  caofinvl  5753  2ndrn  5829  1st2ndbr  5830  cnvf1o  5866  f1o2ndf1  5869  mpt2xopoveq  5878  sprmpt2  5880  dftpos4  5901  tpostpos  5902  tposf12  5907  dfsmo2  5925  smores  5930  tfrlem1  5946  tfrlem3ag  5947  tfrlem3a  5948  tfrlemisucaccv  5962  tfrlemi1  5969  tfrexlem  5971  rdgivallem  5991  frecabex  6007  frectfr  6008  frecrdg  6015  freccl  6016  oawordi  6072  nntri3  6098  nndifsnid  6103  nnaordi  6104  nnaordex  6123  nnawordex  6124  nnm00  6125  ersymb  6143  ertr  6144  erref  6149  iserd  6155  swoer  6157  erth  6173  iinerm  6201  erinxp  6203  ecinxp  6204  qsel  6206  qliftel  6209  qliftfun  6211  dom3  6279  ssdomg  6281  cnven  6311  phplem4dom  6348  phpm  6351  phpelm  6352  fidifsnen  6355  fidifsnid  6356  fin0  6369  fin0or  6370  en2eqpr  6380  fientri3  6381  unsnfidcex  6385  unsnfidcel  6386  fnfi  6388  relcnvfi  6391  f1dmvrnfibi  6393  suplubti  6413  suplub2ti  6414  supelti  6415  supisolem  6421  supisoex  6422  infglbti  6438  ordiso2  6446  dmaddpqlem  6567  nqpi  6568  mulcanenq  6575  ltaddnq  6597  ltexnqq  6598  prarloclemarch2  6609  ltrnqg  6610  ltnnnq  6613  enq0sym  6622  nqnq0pi  6628  nq0nn  6632  mulcanenq0ec  6635  addnq0mo  6637  mulnq0mo  6638  addnnnq0  6639  prloc  6681  prarloclemlt  6683  prarloclemlo  6684  ltdfpr  6696  genplt2i  6700  genpml  6707  genpmu  6708  addnqprllem  6717  addnqprulem  6718  addnqprl  6719  addnqpru  6720  nqprloc  6735  appdivnq  6753  appdiv0nq  6754  mulnqprl  6758  mulnqpru  6759  distrlem1prl  6772  distrlem1pru  6773  ltprordil  6779  1idprl  6780  1idpru  6781  ltexprlemrl  6800  ltexprlemru  6802  ltexpri  6803  addcanprleml  6804  addcanprlemu  6805  recexprlem1ssl  6823  recexpr  6828  aptiprlemu  6830  archpr  6833  cauappcvgprlemopl  6836  cauappcvgprlemdisj  6841  cauappcvgprlemloc  6842  cauappcvgprlemladdfu  6844  cauappcvgprlemladdfl  6845  cauappcvgprlemladdru  6846  cauappcvgprlemladdrl  6847  caucvgprlemm  6858  caucvgprlemopl  6859  caucvgprlemloc  6865  caucvgprlemladdfu  6867  caucvgprlemladdrl  6868  caucvgprlemlim  6871  caucvgprprlemval  6878  caucvgprprlemml  6884  caucvgprprlemopl  6887  caucvgprprlemopu  6889  caucvgprprlemloc  6893  caucvgprprlemexbt  6896  caucvgprprlemexb  6897  caucvgprprlemaddq  6898  caucvgprprlemlim  6901  addsrmo  6920  mulsrmo  6921  addsrpr  6922  mulsrpr  6923  0idsr  6944  1idsr  6945  recexsrlem  6951  addgt0sr  6952  srpospr  6959  prsradd  6962  prsrlt  6963  caucvgsrlemfv  6967  caucvgsrlemgt1  6971  caucvgsrlemoffval  6972  caucvgsrlemoffcau  6974  caucvgsrlemoffres  6976  rereceu  7055  axarch  7057  nntopi  7060  axcaucvglemval  7063  muladd11r  7264  cnegexlem1  7283  cnegex  7286  negeu  7299  pncan  7314  pncan3  7316  npcan  7317  addid0  7477  negf1o  7486  mulneg1  7499  lelttrdi  7530  ltnegcon2  7568  add20  7578  subge0  7579  lesub0  7583  reapval  7676  recexre  7678  apreap  7687  ltmul1a  7691  reapneg  7697  cru  7702  apsym  7706  apcotr  7707  apadd1  7708  apneg  7711  mulext1  7712  apti  7722  gt0ap0  7725  ap0gt0  7738  recexap  7743  divmulassap  7783  divmulasscomap  7784  rerecclap  7818  recgt0  7928  prodgt0gt0  7929  lemul1a  7936  lemul12a  7940  lt2msq  7964  ltrec1  7966  recreclt  7978  negiso  8033  creui  8037  cju  8038  avglt2  8270  un0addcl  8321  nn0ge2m1nn  8348  nn0nndivcl  8350  elnn0z  8364  peano2z  8387  elz2  8419  suprzclex  8445  peano5uzti  8455  zindd  8465  eluzadd  8647  nn0pzuz  8675  supinfneg  8683  infsupneg  8684  eluz2b2  8690  eqreznegel  8699  nn0ge2m1nnALT  8703  divfnzn  8706  qmulz  8708  qapne  8724  qreccl  8727  cnref1o  8733  ge0p1rp  8765  xrltso  8871  z2ge  8893  xltnegi  8902  ixxssixx  8925  lincmb01cmp  9025  iccf1o  9026  zltaddlt1le  9028  fztri3or  9058  fzdcel  9059  fznlem  9060  fzn  9061  uzsubsubfz  9066  fzsplit2  9069  fzopth  9079  fzdifsuc  9098  fzrev2i  9103  elfz1b  9107  fzneuz  9118  fzrevral  9122  ige2m1fz  9127  elfz0ubfz0  9136  elfz0fzfz0  9137  4fvwrd4  9150  2ffzeq  9151  fzospliti  9185  fzosplit  9186  fzo1fzo0n0  9192  fzonmapblen  9196  fzoaddel  9201  fzosubel  9203  fzosubel3  9205  elfzodifsumelfzo  9210  elfzom1elp1fzo  9211  elfzom1p1elfzo  9223  elfzonelfzo  9239  peano2fzor  9241  exfzdc  9249  fvinim0ffz  9250  qtri3or  9252  qbtwnzlemstep  9257  rebtwn2zlemstep  9261  qbtwnxr  9266  flqge  9284  flqltnz  9289  flqaddz  9299  btwnzge0  9302  flltdivnn0lt  9306  intfracq  9322  flqdiv  9323  modqid0  9352  q0mod  9357  q1mod  9358  modqmuladdim  9369  modqmuladdnn0  9370  q2txmodxeq0  9386  q2submod  9387  modifeq2int  9388  modqsubdir  9395  modsumfzodifsn  9398  addmodlteq  9400  frec2uzzd  9402  frec2uzuzd  9404  frec2uzrand  9407  frec2uzf1od  9408  frecuzrdgrrn  9410  frec2uzrdg  9411  frecuzrdgfn  9414  frecuzrdgcl  9415  frecuzrdgsuc  9417  frecfzennn  9419  uzsinds  9428  iseqf  9444  iseqss  9446  iseqfeq2  9449  iseqfeq  9451  isermono  9457  iseqsplit  9458  iseqid3s  9466  iseqid  9467  iseqhomo  9468  iseqz  9469  expivallem  9477  expival  9478  expinnval  9479  expp1  9483  rpexpcl  9495  expaddzaplem  9519  leexp1a  9531  exple1  9532  subsq  9581  binom2  9585  binom3  9590  bernneq3  9595  expnbnd  9596  expcan  9644  nn0opthd  9649  faclbnd  9668  faclbnd6  9671  facubnd  9672  facavg  9673  bcval  9676  bccmpl  9681  ibcval5  9690  bcpasc  9693  shftfvalg  9706  ovshftex  9707  shftdm  9710  shftfib  9711  shftval  9713  shftval5  9717  shftf  9718  2shfti  9719  crre  9744  rereb  9750  cjreim2  9791  cjap  9793  caucvgrelemrec  9865  caucvgrelemcau  9866  caucvgre  9867  cvg1nlemf  9869  cvg1nlemres  9871  uzin2  9873  rexuz3  9876  recvguniq  9881  sqrt0  9890  resqrexlemdecn  9898  resqrexlemlo  9899  resqrexlemcalc3  9902  resqrexlemnm  9904  resqrexlemcvg  9905  resqrexlemoverl  9907  resqrexlemglsq  9908  resqrexlemga  9909  resqrex  9912  sqrtgt0  9920  absrpclap  9947  absext  9949  absmul  9955  leabs  9960  nn0abscl  9971  ltabs  9973  abslt  9974  absle  9975  abssubap0  9976  abstri  9990  cau3lem  10000  caubnd2  10003  maxabsle  10090  maxabslemlub  10093  maxabslemval  10094  maxcl  10096  maxleastb  10100  maxltsup  10104  rexanre  10106  rexico  10107  fimaxre2  10109  minmax  10112  min2inf  10114  clim  10120  climi2  10127  climconst2  10130  climuni  10132  climmpt  10139  climshftlemg  10141  climres  10142  climcn1  10147  subcn2  10150  cn1lem  10152  climadd  10164  climmul  10165  climsub  10166  climle  10172  climsqz  10173  climsqz2  10174  clim2iser  10175  clim2iser2  10176  iiserex  10177  iisermulc2  10178  iserile  10180  iserige0  10181  climub  10182  climserile  10183  climrecvg1n  10185  climcvg1nlem  10186  serif0  10189  dvdsval2  10198  dvdsdc  10203  moddvds  10204  zdvdsdc  10216  dvdscmul  10222  dvdsmulc  10223  dvdscmulr  10224  dvdsmulcr  10225  modmulconst  10227  dvdsadd  10238  dvdsadd2b  10242  dvdslelemd  10243  dvdsle  10244  dvdsabseq  10247  dvdseq  10248  divconjdvds  10249  dvds1  10253  fzo0dvdseq  10257  dvdsmod  10262  oddm1even  10274  mod2eq1n2dvds  10279  evennn02n  10282  evennn2n  10283  divalglemnn  10318  divalglemnqt  10320  divalglemeunn  10321  divalglemex  10322  divalglemeuneg  10323  divalg  10324  divalgmod  10327  modremain  10329  infssuzex  10345  gcdsupex  10349  gcdsupcl  10350  gcdval  10351  dvdslegcd  10356  gcdnncl  10359  gcdneg  10373  gcdaddm  10375  gcd1  10378  bezoutlemnewy  10385  bezoutlemmain  10387  bezoutlemex  10390  bezoutlemzz  10391  bezoutlemaz  10392  bezoutlembz  10393  bezoutlembi  10394  bezoutlemle  10397  bezoutlemsup  10398  gcdass  10404  gcdzeq  10411  dvdsmulgcd  10414  bezoutr1  10422  ialgrp1  10428  ialgcvga  10433  eucalgval2  10435  eucalgf  10437  eucalglt  10439  lcmval  10445  lcmledvds  10452  lcmneg  10456  lcmgcd  10460  lcmid  10462  coprmgcdb  10470  ncoprmgcdne1b  10471  mulgcddvds  10476  rpmulgcd2  10477  qredeq  10478  divgcdcoprm0  10483  divgcdcoprmex  10484  cncongr1  10485  cncongr2  10486  isprm2lem  10498  prmind2  10502  sqnprm  10517  isprm6  10526  prmdvdsexp  10527  prmfac1  10531  rpexp  10532  rpexp1i  10533  sqrt2irr  10541  pw2dvdslemn  10543  pw2dvdseulemle  10545  oddpwdclemxy  10547  oddpwdclemdc  10551  oddpwdc  10552  znege1  10556  sqrt2irraplemnn  10557  sqrt2irrap  10558  bj-indind  10727  bj-omtrans  10751  qdencn  10785