MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simpllr 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  6007  f1o2ndf1  6413  tz7.49  6661  omabs  6849  omxpenlem  7168  fopwdom  7175  findcard3  7309  frfi  7311  finsschain  7371  marypha1lem  7396  wdomtr  7499  cantnfp1  7593  harcard  7821  numacn  7886  infunsdom1  8049  cofsmo  8105  sornom  8113  ssfin4  8146  fin1a2lem11  8246  fin1a2lem13  8248  ttukeylem5  8349  fpwwe2lem13  8473  pwfseq  8495  00id  9197  addid1  9202  cnegex  9203  negeu  9252  add20  9496  ltmul12a  9822  lediv12a  9859  cru  9948  qextltlem  10744  xleadd1a  10788  xmullem  10799  xlemul1a  10823  ixxss12  10892  ioodisj  10982  seqf1o  11319  mulexpz  11375  leexp1a  11393  faclbnd  11536  abs3lem  12097  cau3lem  12113  rlim3  12247  ello12  12265  lo1bdd2  12273  elo12  12276  rlimconst  12293  isercoll  12416  climcau  12419  climbdd  12420  summolem2  12465  fsumconst  12528  o1fsum  12547  incexclem  12571  bitsfzo  12902  dvdsmulgcd  13009  pc2dvds  13207  pcz  13209  pcadd  13213  pcfac  13223  vdwmc2  13302  vdwlem2  13305  vdwlem10  13313  vdw  13317  ramcl  13352  firest  13615  prdsval  13633  mreexd  13822  mreexexlemd  13824  iscat  13852  cidfval  13856  iscatd2  13861  catcocl  13865  catass  13866  catpropd  13890  cidpropd  13891  moni  13917  monpropd  13918  issubc  13990  subccocl  13997  funcco  14023  funcpropd  14052  fullpropd  14072  nati  14107  natpropd  14128  fucpropd  14129  xpcpropd  14260  curfuncf  14290  curf2ndf  14299  yonffthlem  14334  acsfiindd  14558  mndpropd  14676  mhmeql  14719  isgrpinv  14810  conjnmzb  14995  gass  15033  dfod2  15155  gexdvds  15173  sylow3lem2  15217  efgredlem  15334  efgredeu  15339  oddvdssubg  15425  dprdfcntz  15528  pgpfaclem3  15596  isrng  15623  dvdsrmul1  15713  issubdrg  15848  islmhm2  16069  lmhmeql  16086  lssacsex  16171  issubassa2  16358  opsrval  16490  isphl  16814  cctop  17025  neiptoptop  17150  neiptopreu  17152  tgrest  17177  ordtrest2lem  17221  cnss1  17294  cncnp  17298  isnrm3  17377  uncmp  17420  cmpfi  17425  iuncon  17444  1stcrest  17469  subislly  17497  islly2  17500  cldllycmp  17511  lly1stc  17512  llycmpkgen2  17535  kgencn  17541  xkoccn  17604  ptcnplem  17606  pthaus  17623  txhaus  17632  txkgen  17637  xkohaus  17638  xkococnlem  17644  txcon  17674  regr1lem2  17725  kqreglem1  17726  reghmph  17778  nrmhmph  17779  trfil2  17872  ufileu  17904  flimopn  17960  flimcf  17967  fclscf  18010  ufilcmp  18017  cnpfcf  18026  cnextfun  18048  tgpmulg  18076  symgtgp  18084  tgpt0  18101  divstgplem  18103  ustex2sym  18199  ustex3sym  18200  trust  18212  restutop  18220  restutopopn  18221  ustuqtop2  18225  ustuqtop4  18227  utop3cls  18234  utopreg  18235  cstucnd  18267  ucncn  18268  trcfilu  18277  neipcfilu  18279  ismet2  18316  metequiv2  18493  metcnp  18524  metcnp2  18525  metcnpi3  18529  txmetcnp  18530  metusttoOLD  18540  metustto  18541  metustsymOLD  18544  metustsym  18545  metustOLD  18550  metust  18551  cfilucfilOLD  18552  cfilucfil  18553  metuel2  18562  metutopOLD  18565  psmetutop  18566  restmetu  18570  metucnOLD  18571  metucn  18572  ngptgp  18630  tngngp  18648  nmoleub  18718  icccmp  18809  reconnlem2  18811  reconn  18812  xmetdcn2  18821  metdseq0  18837  metdscn  18839  elcncf2  18873  cncfmet  18891  cnheibor  18933  nmoleub2lem2  19077  nmoleub3  19080  iscfil2  19172  iscfil3  19179  cfilfcls  19180  equivcfil  19205  caubl  19213  bcthlem5  19234  pmltpc  19300  ovollb2  19338  ovoliunnul  19356  ovolicc2lem4  19369  volsup  19403  ioorf  19418  dyadss  19439  dyaddisjlem  19440  mbfposr  19497  cncombf  19503  mbflimsup  19511  i1fmulclem  19547  mbfi1fseqlem4  19563  iblss2  19650  ellimc2  19717  ellimc3  19719  dvnadd  19768  dvmptfsum  19812  dvferm1  19822  dvferm2  19824  fta1g  20043  plyeq0lem  20082  plydivex  20167  fta1  20178  aalioulem2  20203  aalioulem3  20204  ulmuni  20261  ulmbdd  20267  ulmdvlem3  20271  mtest  20273  abelthlem8  20308  pilem3  20322  efopn  20502  cxpmul2z  20535  cxpcn3lem  20584  jensen  20780  isppw2  20851  sqf11  20875  mersenne  20964  dchrelbas3  20975  dchrptlem1  21001  dchrpt  21004  lgsval2lem  21043  lgsdchrval  21084  lgsquad3  21098  2sqb  21115  pntrsumbnd2  21214  pntpbnd  21235  pntibnd  21240  usgra1  21346  usgrares1  21377  nbgraf1olem5  21408  pthdepisspth  21527  iseupa  21640  eupath2  21655  isgrp2d  21776  smcnlem  22146  0lno  22244  ubthlem1  22325  ubthlem3  22327  chocunii  22756  occl  22759  5oalem1  23109  3oalem2  23118  nmopub2tALT  23365  nmfnleub2  23382  lnconi  23489  kbass5  23576  mdslmd1lem1  23781  mdslmd1lem2  23782  cdj1i  23889  disjabrex  23977  disjabrexf  23978  xrofsup  24079  xrge0addgt0  24167  subofld  24198  pstmxmet  24245  sqsscirc1  24259  pnfneige0  24289  lmxrge0  24290  lmdvg  24291  qqhval2  24319  esumcst  24408  esumfsup  24413  esumcvg  24429  sigaclfu2  24457  insiga  24473  measinb  24528  imambfm  24565  dstrvprob  24682  lgambdd  24774  lgamucov  24775  derangenlem  24810  sconpi1  24879  cvmsss2  24914  cvmopnlem  24918  cvmlift3lem7  24965  fprodconst  25255  axsegcon  25770  axeuclidlem  25805  axcontlem2  25808  ifscgr  25882  cgrxfr  25893  btwnconn1lem13  25937  outsideofeu  25969  mblfinlem  26143  itg2addnclem  26155  ftc1cnnc  26178  neibastop2lem  26279  sstotbnd2  26373  equivtotbnd  26377  isbnd3  26383  ssbnd  26387  totbndbnd  26388  cntotbnd  26395  heibor1lem  26408  rrncmslem  26431  mzpindd  26693  mzpsubst  26695  mzpcompact2lem  26698  eldioph2b  26711  irrapxlem3  26777  irrapxlem5  26779  pellex  26788  pell1234qrdich  26814  pell14qrexpcl  26820  congabseq  26929  jm2.26a  26961  jm2.26lem3  26962  rmydioph  26975  uvcf1  27109  lindfmm  27165  lnrfg  27191  hbt  27202  fnchoice  27567  cncmpmax  27570  climrec  27596  climsuse  27601  stoweidlem7  27623  stoweidlem34  27650  stoweidlem52  27668  stoweidlem60  27676  wallispilem3  27683  swrdswrdlem  28010  usgra2pthspth  28035  el2spthonot  28067  usg2wotspth  28081  frgrancvvdeqlem9  28144  lssats  29495  lsat0cv  29516  lkrlss  29578  lfl1dim  29604  lfl1dim2N  29605  lkrpssN  29646  hlhgt2  29871  3dim2  29950  2dim  29952  lplncvrlvol  30098  paddasslem11  30312  pmapjat1  30335  2polssN  30397  pclfinclN  30432  pexmidlem8N  30459  lhpexle1lem  30489  4atex  30558  ltrnid  30617  trlator0  30653  cdlemg2cex  31073  tendodi1  31266  tendodi2  31267  diblss  31653  dihopelvalcpre  31731  dihatexv  31821  mapdval4N  32115
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