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

Theorem simpllr 736
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 448 . 2  |-  ( (
ph  /\  ps )  ->  ps )
21ad2antrr 707 1  |-  ( ( ( ( ph  /\  ps )  /\  ch )  /\  th )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  simp-4r  744  soisoi  6048  f1o2ndf1  6454  tz7.49  6702  omabs  6890  omxpenlem  7209  fopwdom  7216  findcard3  7350  frfi  7352  finsschain  7413  marypha1lem  7438  wdomtr  7543  cantnfp1  7637  harcard  7865  numacn  7930  infunsdom1  8093  cofsmo  8149  sornom  8157  ssfin4  8190  fin1a2lem11  8290  fin1a2lem13  8292  ttukeylem5  8393  fpwwe2lem13  8517  pwfseq  8539  00id  9241  addid1  9246  cnegex  9247  negeu  9296  add20  9540  ltmul12a  9866  lediv12a  9903  cru  9992  qextltlem  10788  xleadd1a  10832  xmullem  10843  xlemul1a  10867  ixxss12  10936  ioodisj  11026  seqf1o  11364  mulexpz  11420  leexp1a  11438  faclbnd  11581  abs3lem  12142  cau3lem  12158  rlim3  12292  ello12  12310  lo1bdd2  12318  elo12  12321  rlimconst  12338  isercoll  12461  climcau  12464  climbdd  12465  summolem2  12510  fsumconst  12573  o1fsum  12592  incexclem  12616  bitsfzo  12947  dvdsmulgcd  13054  pc2dvds  13252  pcz  13254  pcadd  13258  pcfac  13268  vdwmc2  13347  vdwlem2  13350  vdwlem10  13358  vdw  13362  ramcl  13397  firest  13660  prdsval  13678  mreexd  13867  mreexexlemd  13869  iscat  13897  cidfval  13901  iscatd2  13906  catcocl  13910  catass  13911  catpropd  13935  cidpropd  13936  moni  13962  monpropd  13963  issubc  14035  subccocl  14042  funcco  14068  funcpropd  14097  fullpropd  14117  nati  14152  natpropd  14173  fucpropd  14174  xpcpropd  14305  curfuncf  14335  curf2ndf  14344  yonffthlem  14379  acsfiindd  14603  mndpropd  14721  mhmeql  14764  isgrpinv  14855  conjnmzb  15040  gass  15078  dfod2  15200  gexdvds  15218  sylow3lem2  15262  efgredlem  15379  efgredeu  15384  oddvdssubg  15470  dprdfcntz  15573  pgpfaclem3  15641  isrng  15668  dvdsrmul1  15758  issubdrg  15893  islmhm2  16114  lmhmeql  16131  lssacsex  16216  issubassa2  16403  opsrval  16535  isphl  16859  cctop  17070  neiptoptop  17195  neiptopreu  17197  tgrest  17223  ordtrest2lem  17267  cnss1  17340  cncnp  17344  isnrm3  17423  uncmp  17466  cmpfi  17471  iuncon  17491  1stcrest  17516  subislly  17544  islly2  17547  cldllycmp  17558  lly1stc  17559  llycmpkgen2  17582  kgencn  17588  xkoccn  17651  ptcnplem  17653  pthaus  17670  txhaus  17679  txkgen  17684  xkohaus  17685  xkococnlem  17691  txcon  17721  regr1lem2  17772  kqreglem1  17773  reghmph  17825  nrmhmph  17826  trfil2  17919  ufileu  17951  flimopn  18007  flimcf  18014  fclscf  18057  ufilcmp  18064  cnpfcf  18073  cnextfun  18095  tgpmulg  18123  symgtgp  18131  tgpt0  18148  divstgplem  18150  ustex2sym  18246  ustex3sym  18247  trust  18259  restutop  18267  restutopopn  18268  ustuqtop2  18272  ustuqtop4  18274  utop3cls  18281  utopreg  18282  cstucnd  18314  ucncn  18315  trcfilu  18324  neipcfilu  18326  ismet2  18363  metequiv2  18540  metcnp  18571  metcnp2  18572  metcnpi3  18576  txmetcnp  18577  metusttoOLD  18587  metustto  18588  metustsymOLD  18591  metustsym  18592  metustOLD  18597  metust  18598  cfilucfilOLD  18599  cfilucfil  18600  metuel2  18609  metutopOLD  18612  psmetutop  18613  restmetu  18617  metucnOLD  18618  metucn  18619  ngptgp  18677  tngngp  18695  nmoleub  18765  icccmp  18856  reconnlem2  18858  reconn  18859  xmetdcn2  18868  metdseq0  18884  metdscn  18886  elcncf2  18920  cncfmet  18938  cnheibor  18980  nmoleub2lem2  19124  nmoleub3  19127  iscfil2  19219  iscfil3  19226  cfilfcls  19227  equivcfil  19252  caubl  19260  bcthlem5  19281  pmltpc  19347  ovollb2  19385  ovoliunnul  19403  ovolicc2lem4  19416  volsup  19450  ioorf  19465  dyadss  19486  dyaddisjlem  19487  mbfposr  19544  cncombf  19550  mbflimsup  19558  i1fmulclem  19594  mbfi1fseqlem4  19610  iblss2  19697  ellimc2  19764  ellimc3  19766  dvnadd  19815  dvmptfsum  19859  dvferm1  19869  dvferm2  19871  fta1g  20090  plyeq0lem  20129  plydivex  20214  fta1  20225  aalioulem2  20250  aalioulem3  20251  ulmuni  20308  ulmbdd  20314  ulmdvlem3  20318  mtest  20320  abelthlem8  20355  pilem3  20369  efopn  20549  cxpmul2z  20582  cxpcn3lem  20631  jensen  20827  isppw2  20898  sqf11  20922  mersenne  21011  dchrelbas3  21022  dchrptlem1  21048  dchrpt  21051  lgsval2lem  21090  lgsdchrval  21131  lgsquad3  21145  2sqb  21162  pntrsumbnd2  21261  pntpbnd  21282  pntibnd  21287  usgra1  21393  usgrares1  21424  nbgraf1olem5  21455  pthdepisspth  21574  iseupa  21687  eupath2  21702  isgrp2d  21823  smcnlem  22193  0lno  22291  ubthlem1  22372  ubthlem3  22374  chocunii  22803  occl  22806  5oalem1  23156  3oalem2  23165  nmopub2tALT  23412  nmfnleub2  23429  lnconi  23536  kbass5  23623  mdslmd1lem1  23828  mdslmd1lem2  23829  cdj1i  23936  disjabrex  24024  disjabrexf  24025  xrofsup  24126  xrge0addgt0  24214  subofld  24245  pstmxmet  24292  sqsscirc1  24306  pnfneige0  24336  lmxrge0  24337  lmdvg  24338  qqhval2  24366  esumcst  24455  esumfsup  24460  esumcvg  24476  sigaclfu2  24504  insiga  24520  measinb  24575  imambfm  24612  dstrvprob  24729  lgambdd  24821  lgamucov  24822  derangenlem  24857  sconpi1  24926  cvmsss2  24961  cvmopnlem  24965  cvmlift3lem7  25012  fprodconst  25302  axsegcon  25866  axeuclidlem  25901  axcontlem2  25904  ifscgr  25978  cgrxfr  25989  btwnconn1lem13  26033  outsideofeu  26065  mblfinlem1  26243  itg2addnclem  26256  ftc1cnnc  26279  ftc1anclem7  26286  neibastop2lem  26389  sstotbnd2  26483  equivtotbnd  26487  isbnd3  26493  ssbnd  26497  totbndbnd  26498  cntotbnd  26505  heibor1lem  26518  rrncmslem  26541  mzpindd  26803  mzpsubst  26805  mzpcompact2lem  26808  eldioph2b  26821  irrapxlem3  26887  irrapxlem5  26889  pellex  26898  pell1234qrdich  26924  pell14qrexpcl  26930  congabseq  27039  jm2.26a  27071  jm2.26lem3  27072  rmydioph  27085  uvcf1  27218  lindfmm  27274  lnrfg  27300  hbt  27311  fnchoice  27676  cncmpmax  27679  climrec  27705  climsuse  27710  stoweidlem7  27732  stoweidlem34  27759  stoweidlem52  27777  stoweidlem60  27785  wallispilem3  27792  swrdswrdlem  28198  cshweqdif2s  28271  cshweqrep  28274  usgra2pthspth  28305  el2spthonot  28337  usg2wotspth  28351  frgrancvvdeqlem9  28430  4animp1  28580  4an4132  28582  iunconlem2  29047  lssats  29810  lsat0cv  29831  lkrlss  29893  lfl1dim  29919  lfl1dim2N  29920  lkrpssN  29961  hlhgt2  30186  3dim2  30265  2dim  30267  lplncvrlvol  30413  paddasslem11  30627  pmapjat1  30650  2polssN  30712  pclfinclN  30747  pexmidlem8N  30774  lhpexle1lem  30804  4atex  30873  ltrnid  30932  trlator0  30968  cdlemg2cex  31388  tendodi1  31581  tendodi2  31582  diblss  31968  dihopelvalcpre  32046  dihatexv  32136  mapdval4N  32430
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 178  df-an 361
  Copyright terms: Public domain W3C validator