MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simpllr Unicode version

Theorem simpllr 735
Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
Assertion
Ref Expression
simpllr  |-  ( ( ( ( ph  /\  ps )  /\  ch )  /\  th )  ->  ps )

Proof of Theorem simpllr
StepHypRef Expression
1 simpr 447 . 2  |-  ( (
ph  /\  ps )  ->  ps )
21ad2antrr 706 1  |-  ( ( ( ( ph  /\  ps )  /\  ch )  /\  th )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  simp-4r  743  soisoi  5841  tz7.49  6473  omabs  6661  undom  6966  omxpenlem  6979  fopwdom  6986  findcard3  7116  frfi  7118  finsschain  7178  marypha1lem  7202  wdomtr  7305  cantnfp1  7399  harcard  7627  numacn  7692  infunsdom1  7855  cofsmo  7911  sornom  7919  ssfin4  7952  isf32lem2  7996  fin1a2lem11  8052  fin1a2lem13  8054  ttukeylem3  8154  ttukeylem5  8156  fpwwe2lem13  8280  pwfseq  8302  gchina  8337  r1limwun  8374  00id  9003  addid1  9008  cnegex  9009  negeu  9058  add20  9302  ltmul12a  9628  lediv12a  9665  cru  9754  qextltlem  10545  xleadd1a  10589  xmullem  10600  xlemul1a  10624  ixxss12  10692  ioodisj  10781  seqf1o  11103  mulexpz  11158  leexp1a  11176  faclbnd  11319  abs3lem  11838  cau3lem  11854  rlim3  11988  ello12  12006  lo1bdd2  12014  elo12  12017  rlimconst  12034  o1of2  12102  isercoll  12157  climcau  12160  summolem2  12205  fsumconst  12268  o1fsum  12287  incexclem  12311  bitsfzo  12642  dvdsmulgcd  12749  isprm5  12807  pc2dvds  12947  pcz  12949  pcadd  12953  pcfac  12963  vdwmc2  13042  vdwlem2  13045  vdwlem10  13053  vdw  13057  ramval  13071  ramcl  13092  firest  13353  prdsval  13371  mreexd  13560  mreexexlemd  13562  iscat  13590  cidfval  13594  iscatd2  13599  catcocl  13603  catass  13604  catpropd  13628  cidpropd  13629  moni  13655  monpropd  13656  issubc  13728  subccocl  13735  funcco  13761  funcpropd  13790  fullpropd  13810  nati  13845  natpropd  13866  fucpropd  13867  xpcpropd  13998  curfuncf  14028  curf2ndf  14037  yonffthlem  14072  acsfiindd  14296  mndpropd  14414  mhmeql  14457  isgrpinv  14548  conjnmzb  14733  gass  14771  gasubg  14772  dfod2  14893  gexdvds  14911  sylow3lem2  14955  efgredlem  15072  efgredeu  15077  oddvdssubg  15163  dprdfcntz  15266  pgpfaclem3  15334  isrng  15361  dvdsrmul1  15451  issubdrg  15586  islmhm2  15811  lmhmeql  15828  lssacsex  15913  issubassa2  16100  opsrval  16232  isphl  16548  cctop  16759  tgrest  16906  ordtrest2lem  16949  iscncl  17014  cncls  17019  cnntr  17020  cnss1  17021  cncnp  17025  isnrm3  17103  uncmp  17146  cmpfi  17151  iuncon  17170  1stcfb  17187  1stcrest  17195  subislly  17223  islly2  17226  cldllycmp  17237  lly1stc  17238  llycmpkgen2  17261  kgencn  17267  xkoccn  17329  ptcnplem  17331  pthaus  17348  txhaus  17357  txkgen  17362  xkohaus  17363  xkococnlem  17369  txcon  17399  regr1lem2  17447  kqreglem1  17448  reghmph  17500  nrmhmph  17501  trfil2  17598  ufileu  17630  flimopn  17686  fbflim  17687  flimcf  17693  fclsbas  17732  fclscf  17736  ufilcmp  17743  cnpfcf  17752  tgpmulg  17792  symgtgp  17800  tgpt0  17817  divstgplem  17819  ismet2  17914  metequiv2  18072  metcnp  18103  metcnp2  18104  metcnpi3  18108  txmetcnp  18109  ngptgp  18168  tngngp  18186  nmoi  18253  nmoleub  18256  icccmp  18346  reconnlem2  18348  reconn  18349  xmetdcn2  18358  metdseq0  18374  metdscn  18376  elcncf2  18410  cncfmet  18428  cnheibor  18469  nmoleub2lem2  18613  nmoleub3  18616  iscfil2  18708  fgcfil  18713  iscfil3  18715  cfilfcls  18716  equivcfil  18741  equivcau  18742  caubl  18749  bcthlem5  18766  pmltpc  18826  ovollb2  18864  ovoliunnul  18882  ovolicc2lem4  18895  volsup  18929  ioorf  18944  dyadss  18965  dyaddisjlem  18966  dyadmax  18969  mbfposr  19023  cncombf  19029  mbflimsup  19037  i1fmulclem  19073  mbfi1fseqlem4  19089  itg2cnlem1  19132  iblss  19175  iblss2  19176  ellimc2  19243  ellimc3  19245  dvnadd  19294  dvmptfsum  19338  dvferm1  19348  dvferm2  19350  fta1g  19569  plyeq0lem  19608  plydivex  19693  fta1  19704  aannenlem1  19724  aalioulem2  19729  aalioulem3  19730  ulmbdd  19791  ulmdvlem3  19795  mtest  19797  abelthlem8  19831  pilem3  19845  efopn  20021  cxpmul2z  20054  cxpcn3lem  20103  jensen  20299  isppw2  20369  sqf11  20393  mersenne  20482  dchrelbas3  20493  dchrptlem1  20519  dchrpt  20522  lgsval2lem  20561  lgsqr  20601  lgsdchrval  20602  lgsquad3  20616  2sqb  20633  pntrsumbnd2  20732  pntpbnd  20753  pntibnd  20758  pntlem3  20774  isgrp2d  20918  smcnlem  21286  0lno  21384  ubthlem1  21465  ubthlem3  21467  chocunii  21896  occl  21899  5oalem1  22249  3oalem2  22258  nmopub2tALT  22505  nmfnleub2  22522  lnconi  22629  kbass5  22716  mdslmd1lem1  22921  mdslmd1lem2  22922  cdj1i  23029  xrofsup  23270  sqsscirc1  23307  xrge0addgt0  23346  disjabrex  23374  disjabrexf  23375  pnfneige0  23389  lmxrge0  23390  lmdvg  23391  esumcst  23451  esumcvg  23469  sigaclfu2  23497  insiga  23513  measinb  23563  imambfm  23582  dstrvprob  23687  derangenlem  23717  sconpi1  23785  cvmsss2  23820  cvmopnlem  23824  cvmlift2lem12  23860  cvmlift3lem7  23871  iseupa  23896  eupath2  23919  axsegcon  24627  axeuclidlem  24662  axcontlem2  24665  ifscgr  24739  cgrxfr  24750  btwnconn1lem13  24794  outsideofeu  24826  itg2addnclem  25003  ftc1cnnc  25025  mgmlion  25440  muldisc  25584  glmrngo  25585  tcnvec  25793  idmon  25920  pdiveql  26271  neibastop2lem  26412  neibastop2  26413  neibastop3  26414  sstotbnd2  26601  equivtotbnd  26605  isbnd3  26611  ssbnd  26615  totbndbnd  26616  cntotbnd  26623  heibor1lem  26636  rrncmslem  26659  mzpindd  26927  mzpsubst  26929  mzpcompact2lem  26932  eldioph2b  26945  diophren  26999  irrapxlem3  27012  irrapxlem4  27013  irrapxlem5  27014  pellex  27023  pell1234qrdich  27049  pell14qrexpcl  27055  congabseq  27164  jm2.26a  27196  jm2.26lem3  27197  rmydioph  27210  uvcf1  27344  lindfmm  27400  lnrfg  27426  hbt  27437  fnchoice  27803  cncmpmax  27806  climrec  27832  climsuse  27837  stoweidlem7  27859  stoweidlem34  27886  stoweidlem52  27904  stoweidlem60  27912  wallispilem3  27919  usgra1  28253  pthdepisspth  28360  lssats  29824  lsat0cv  29845  lkrlss  29907  lfl1dim  29933  lfl1dim2N  29934  lkrpssN  29975  hlhgt2  30200  3dim2  30279  2dim  30281  lplncvrlvol  30427  paddasslem11  30641  pmapjat1  30664  2polssN  30726  pclfinclN  30761  pexmidlem8N  30788  lhpexle1lem  30818  lhpmatb  30842  4atex  30887  ltrnid  30946  trlator0  30982  cdlemf2  31373  cdlemg2cex  31402  tendodi1  31595  tendodi2  31596  diaglbN  31867  diaintclN  31870  dibglbN  31978  dibintclN  31979  diblss  31982  dihlsscpre  32046  dihopelvalcpre  32060  dihglblem5aN  32104  dihglblem2aN  32105  dih1dimatlem  32141  dihatexv  32150  lcfl8  32314  mapdval4N  32444
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator