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

Theorem simpllr 758
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 461 . 2  |-  ( (
ph  /\  ps )  ->  ps )
21ad2antrr 725 1  |-  ( ( ( ( ph  /\  ps )  /\  ch )  /\  th )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  simp-4r  766  soisoi  6210  f1o2ndf1  6888  tfrlem1  7042  tz7.49  7107  omabs  7293  omxpenlem  7615  fopwdom  7622  findcard3  7759  frfi  7761  finsschain  7823  marypha1lem  7889  wdomtr  7997  cantnfp1  8096  cantnfp1OLD  8122  harcard  8355  numacn  8426  infunsdom1  8589  cofsmo  8645  sornom  8653  ssfin4  8686  fin1a2lem11  8786  fin1a2lem13  8788  ttukeylem5  8889  fpwwe2lem13  9016  pwfseq  9038  mulcmpblnr  9444  00id  9750  addid1  9755  cnegex  9756  negeu  9806  add20  10060  ltmul12a  10394  lediv12a  10434  cru  10524  qextltlem  11397  xleadd1a  11441  xmullem  11452  xlemul1a  11476  ixxss12  11545  ioodisj  11646  fsuppmapnn0fz  12065  seqf1o  12111  mulexpz  12168  leexp1a  12186  faclbnd  12330  swrdswrdlem  12641  abs3lem  13127  cau3lem  13143  rlim3  13277  ello12  13295  lo1bdd2  13303  elo12  13306  rlimconst  13323  isercoll  13446  climcau  13449  climbdd  13450  summolem2  13494  fsumconst  13561  o1fsum  13583  incexclem  13604  bitsfzo  13937  dvdsmulgcd  14044  pc2dvds  14254  pcz  14256  pcadd  14260  pcfac  14270  vdwmc2  14349  vdwlem2  14352  vdwlem10  14360  vdw  14364  ramcl  14399  sbcie3s  14527  firest  14681  prdsval  14703  mreexd  14890  mreexexlemd  14892  iscat  14920  cidfval  14924  iscatd2  14929  catcocl  14933  catass  14934  catpropd  14958  cidpropd  14959  moni  14985  monpropd  14986  issubc  15058  subccocl  15065  funcco  15091  funcpropd  15120  fullpropd  15140  nati  15175  natpropd  15196  fucpropd  15197  xpcpropd  15328  curfuncf  15358  curf2ndf  15367  yonffthlem  15402  acsfiindd  15657  mndpropd  15756  mhmeql  15802  isgrpinv  15898  conjnmzb  16093  gass  16131  symgextf  16234  dfod2  16379  gexdvds  16397  sylow3lem2  16441  efgredlem  16558  efgredeu  16563  oddvdssubg  16651  dprdfcntz  16836  dprdfcntzOLD  16842  pgpfaclem3  16921  issrg  16946  isrng  16987  dvdsrmul1  17083  issubdrg  17234  islmhm2  17464  lmhmeql  17481  lssacsex  17570  issubassa2  17762  opsrval  17907  isphl  18427  uvcf1  18587  lindfmm  18626  scmatmats  18777  smatvscl  18790  mdetunilem7  18884  gsummatr01lem4  18924  m2cpmfo  19021  decpmatmulsumfsupp  19038  pmatcollpw3fi1lem1  19051  pm2mpf1lem  19059  mp2pm2mplem4  19074  pm2mpghm  19081  pm2mpmhmlem1  19083  pm2mpmhmlem2  19084  chfacfscmulfsupp  19124  chfacfpmmulfsupp  19128  cctop  19270  neiptoptop  19395  neiptopreu  19397  tgrest  19423  ordtrest2lem  19467  cnss1  19540  cncnp  19544  isnrm3  19623  uncmp  19666  cmpfi  19671  iuncon  19692  1stcrest  19717  subislly  19745  islly2  19748  cldllycmp  19759  lly1stc  19760  llycmpkgen2  19783  kgencn  19789  xkoccn  19852  ptcnplem  19854  pthaus  19871  txhaus  19880  txkgen  19885  xkohaus  19886  xkococnlem  19892  txcon  19922  regr1lem2  19973  kqreglem1  19974  reghmph  20026  nrmhmph  20027  trfil2  20120  ufileu  20152  flimopn  20208  flimcf  20215  fclscf  20258  ufilcmp  20265  cnpfcf  20274  cnextfun  20296  tgpmulg  20324  symgtgp  20332  tgpt0  20349  divstgplem  20351  ustex2sym  20451  ustex3sym  20452  trust  20464  restutop  20472  restutopopn  20473  ustuqtop2  20477  ustuqtop4  20479  utop3cls  20486  utopreg  20487  cstucnd  20519  ucncn  20520  trcfilu  20529  neipcfilu  20531  ismet2  20568  metequiv2  20745  metcnp  20776  metcnp2  20777  metcnpi3  20781  txmetcnp  20782  metusttoOLD  20792  metustto  20793  metustsymOLD  20796  metustsym  20797  metustOLD  20802  metust  20803  cfilucfilOLD  20804  cfilucfil  20805  metuel2  20814  metutopOLD  20817  psmetutop  20818  restmetu  20822  metucnOLD  20823  metucn  20824  ngptgp  20882  tngngp  20900  nmoleub  20970  icccmp  21062  reconnlem2  21064  reconn  21065  xmetdcn2  21074  metdseq0  21090  metdscn  21092  elcncf2  21126  cncfmet  21144  cnheibor  21187  nmoleub2lem2  21331  nmoleub3  21334  iscfil2  21437  iscfil3  21444  cfilfcls  21445  equivcfil  21470  caubl  21478  bcthlem5  21499  pmltpc  21594  ovollb2  21632  ovoliunnul  21650  ovolicc2lem4  21663  volsup  21698  ioorf  21714  dyadss  21735  dyaddisjlem  21736  mbfposr  21791  cncombf  21797  mbflimsup  21805  i1fmulclem  21841  mbfi1fseqlem4  21857  iblss2  21944  ellimc2  22013  ellimc3  22015  dvnadd  22064  dvmptfsum  22108  dvferm1  22118  dvferm2  22120  fta1g  22300  plyeq0lem  22339  plydivex  22424  fta1  22435  aalioulem2  22460  aalioulem3  22461  ulmuni  22518  ulmbdd  22524  ulmdvlem3  22528  mtest  22530  abelthlem8  22565  pilem3  22579  efopn  22764  cxpmul2z  22797  cxpcn3lem  22846  jensen  23043  isppw2  23114  sqf11  23138  mersenne  23227  dchrelbas3  23238  dchrptlem1  23264  dchrpt  23267  lgsval2lem  23306  lgsdchrval  23347  lgsquad3  23361  2sqb  23378  pntrsumbnd2  23477  pntpbnd  23498  pntibnd  23503  istrkgc  23576  istrkgb  23577  tglowdim1i  23617  tgbtwndiff  23622  tgifscgr  23625  tgcgrxfr  23634  lnext  23678  tgbtwnconn1lem3  23685  tgbtwnconn1  23686  legval  23695  legov  23696  legov2  23697  legtrd  23700  legtri3  23701  legso  23709  tglnne  23719  tglndim0  23720  tglinethru  23727  tglnpt2  23731  colline  23740  tglowdim2l  23741  tglowdim2ln  23742  mirreu3  23745  miriso  23760  midexlem  23774  isperp  23794  perpcom  23795  perpneq  23796  isperp2  23797  footex  23800  colperpexlem3  23808  mideulem  23810  mideu  23811  lmieu  23824  f1otrg  23847  f1otrge  23848  axsegcon  23903  axeuclidlem  23938  axcontlem2  23941  usgra1  24046  usgrares1  24083  nbgraf1olem5  24118  pthdepisspth  24249  clwwlkf1  24469  clwwlknscsh  24492  el2spthonot  24543  usg2wotspth  24557  iseupa  24638  eupath2  24653  frgrancvvdeqlem9  24715  friendshipgt3  24795  isgrp2d  24910  smcnlem  25280  0lno  25378  ubthlem1  25459  ubthlem3  25461  chocunii  25892  occl  25895  5oalem1  26245  3oalem2  26254  nmopub2tALT  26501  nmfnleub2  26518  lnconi  26625  kbass5  26712  mdslmd1lem1  26917  mdslmd1lem2  26918  cdj1i  27025  disjabrex  27113  disjabrexf  27114  fgreu  27182  xrge0infss  27245  xrofsup  27247  ressprs  27302  xrge0addgt0  27340  submarchi  27389  isarchi3  27390  archiabllem1  27396  archiabllem2a  27397  gsumle  27430  suborng  27465  isarchiofld  27467  fimaproj  27496  txomap  27497  pstmxmet  27509  sqsscirc1  27523  ordtrest2NEWlem  27537  ordtconlem1  27539  pnfneige0  27566  lmxrge0  27567  lmdvg  27568  qqhval2  27596  qtophaus  27634  esumcst  27708  esumfsup  27713  esumcvg  27729  sigaclfu2  27758  insiga  27774  measinb  27829  imambfm  27870  oms0  27903  eulerpartlemgvv  27952  dstrvprob  28047  sgnmul  28118  sgnsub  28120  signstfvneq0  28166  afsval  28188  lgambdd  28216  lgamucov  28217  derangenlem  28252  sconpi1  28321  cvmsss2  28356  cvmopnlem  28360  cvmlift3lem7  28407  fprodconst  28682  ifscgr  29268  cgrxfr  29279  btwnconn1lem13  29323  outsideofeu  29355  heicant  29624  mblfinlem1  29626  itg2addnclem  29641  ftc1cnnc  29664  ftc1anclem7  29671  neibastop2lem  29779  sstotbnd2  29871  equivtotbnd  29875  isbnd3  29881  ssbnd  29885  totbndbnd  29886  cntotbnd  29893  heibor1lem  29906  rrncmslem  29929  mzpindd  30280  mzpsubst  30283  mzpcompact2lem  30286  eldioph2b  30298  irrapxlem3  30362  irrapxlem5  30364  pellex  30373  pell1234qrdich  30399  pell14qrexpcl  30405  congabseq  30514  jm2.26a  30546  jm2.26lem3  30547  rmydioph  30560  lnrfg  30672  hbt  30683  fnchoice  30982  cncmpmax  30985  climrec  31145  climsuse  31150  islptre  31161  addlimc  31190  0ellimcdiv  31191  icccncfext  31226  cncfiooicclem1  31232  fperdvper  31248  ioodvbdlimc1lem2  31262  ioodvbdlimc2lem  31264  stoweidlem7  31307  stoweidlem34  31334  stoweidlem52  31352  stoweidlem60  31360  wallispilem3  31367  fourierdlem34  31441  fourierdlem38  31445  fourierdlem39  31446  fourierdlem48  31455  fourierdlem50  31457  fourierdlem51  31458  fourierdlem73  31480  fourierdlem76  31483  fourierdlem77  31484  fourierdlem80  31487  fourierdlem87  31494  fourierdlem103  31510  fourierdlem104  31511  usgra2pthspth  31820  isrng0  31981  lindslinindsimp2  32137  snlindsntor  32145  lincresunit2  32152  islindeps2  32157  4animp1  32345  4an4132  32347  iunconlem2  32815  lssats  33809  lsat0cv  33830  lkrlss  33892  lfl1dim  33918  lfl1dim2N  33919  lkrpssN  33960  hlhgt2  34185  3dim2  34264  2dim  34266  lplncvrlvol  34412  paddasslem11  34626  pmapjat1  34649  2polssN  34711  pclfinclN  34746  pexmidlem8N  34773  lhpexle1lem  34803  4atex  34872  ltrnid  34931  trlator0  34967  cdlemg2cex  35387  tendodi1  35580  tendodi2  35581  diblss  35967  dihopelvalcpre  36045  dihatexv  36135  mapdval4N  36429
  Copyright terms: Public domain W3C validator