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  6014  f1o2ndf1  6675  tfrlem1  6827  tz7.49  6892  omabs  7078  omxpenlem  7404  fopwdom  7411  findcard3  7547  frfi  7549  finsschain  7610  marypha1lem  7675  wdomtr  7782  cantnfp1  7881  cantnfp1OLD  7907  harcard  8140  numacn  8211  infunsdom1  8374  cofsmo  8430  sornom  8438  ssfin4  8471  fin1a2lem11  8571  fin1a2lem13  8573  ttukeylem5  8674  fpwwe2lem13  8801  pwfseq  8823  00id  9536  addid1  9541  cnegex  9542  negeu  9592  add20  9843  ltmul12a  10177  lediv12a  10217  cru  10306  qextltlem  11164  xleadd1a  11208  xmullem  11219  xlemul1a  11243  ixxss12  11312  ioodisj  11407  seqf1o  11839  mulexpz  11896  leexp1a  11914  faclbnd  12058  swrdswrdlem  12345  abs3lem  12818  cau3lem  12834  rlim3  12968  ello12  12986  lo1bdd2  12994  elo12  12997  rlimconst  13014  isercoll  13137  climcau  13140  climbdd  13141  summolem2  13185  fsumconst  13249  o1fsum  13268  incexclem  13291  bitsfzo  13623  dvdsmulgcd  13730  pc2dvds  13937  pcz  13939  pcadd  13943  pcfac  13953  vdwmc2  14032  vdwlem2  14035  vdwlem10  14043  vdw  14047  ramcl  14082  sbcie3s  14210  firest  14363  prdsval  14385  mreexd  14572  mreexexlemd  14574  iscat  14602  cidfval  14606  iscatd2  14611  catcocl  14615  catass  14616  catpropd  14640  cidpropd  14641  moni  14667  monpropd  14668  issubc  14740  subccocl  14747  funcco  14773  funcpropd  14802  fullpropd  14822  nati  14857  natpropd  14878  fucpropd  14879  xpcpropd  15010  curfuncf  15040  curf2ndf  15049  yonffthlem  15084  acsfiindd  15339  mndpropd  15438  mhmeql  15483  isgrpinv  15579  conjnmzb  15772  gass  15810  symgextf  15913  dfod2  16056  gexdvds  16074  sylow3lem2  16118  efgredlem  16235  efgredeu  16240  oddvdssubg  16328  dprdfcntz  16487  dprdfcntzOLD  16493  pgpfaclem3  16572  issrg  16597  isrng  16637  dvdsrmul1  16733  issubdrg  16868  islmhm2  17096  lmhmeql  17113  lssacsex  17202  issubassa2  17392  opsrval  17531  isphl  18032  uvcf1  18192  lindfmm  18231  mdetunilem7  18399  gsummatr01lem4  18439  cctop  18585  neiptoptop  18710  neiptopreu  18712  tgrest  18738  ordtrest2lem  18782  cnss1  18855  cncnp  18859  isnrm3  18938  uncmp  18981  cmpfi  18986  iuncon  19007  1stcrest  19032  subislly  19060  islly2  19063  cldllycmp  19074  lly1stc  19075  llycmpkgen2  19098  kgencn  19104  xkoccn  19167  ptcnplem  19169  pthaus  19186  txhaus  19195  txkgen  19200  xkohaus  19201  xkococnlem  19207  txcon  19237  regr1lem2  19288  kqreglem1  19289  reghmph  19341  nrmhmph  19342  trfil2  19435  ufileu  19467  flimopn  19523  flimcf  19530  fclscf  19573  ufilcmp  19580  cnpfcf  19589  cnextfun  19611  tgpmulg  19639  symgtgp  19647  tgpt0  19664  divstgplem  19666  ustex2sym  19766  ustex3sym  19767  trust  19779  restutop  19787  restutopopn  19788  ustuqtop2  19792  ustuqtop4  19794  utop3cls  19801  utopreg  19802  cstucnd  19834  ucncn  19835  trcfilu  19844  neipcfilu  19846  ismet2  19883  metequiv2  20060  metcnp  20091  metcnp2  20092  metcnpi3  20096  txmetcnp  20097  metusttoOLD  20107  metustto  20108  metustsymOLD  20111  metustsym  20112  metustOLD  20117  metust  20118  cfilucfilOLD  20119  cfilucfil  20120  metuel2  20129  metutopOLD  20132  psmetutop  20133  restmetu  20137  metucnOLD  20138  metucn  20139  ngptgp  20197  tngngp  20215  nmoleub  20285  icccmp  20377  reconnlem2  20379  reconn  20380  xmetdcn2  20389  metdseq0  20405  metdscn  20407  elcncf2  20441  cncfmet  20459  cnheibor  20502  nmoleub2lem2  20646  nmoleub3  20649  iscfil2  20752  iscfil3  20759  cfilfcls  20760  equivcfil  20785  caubl  20793  bcthlem5  20814  pmltpc  20909  ovollb2  20947  ovoliunnul  20965  ovolicc2lem4  20978  volsup  21012  ioorf  21028  dyadss  21049  dyaddisjlem  21050  mbfposr  21105  cncombf  21111  mbflimsup  21119  i1fmulclem  21155  mbfi1fseqlem4  21171  iblss2  21258  ellimc2  21327  ellimc3  21329  dvnadd  21378  dvmptfsum  21422  dvferm1  21432  dvferm2  21434  fta1g  21614  plyeq0lem  21653  plydivex  21738  fta1  21749  aalioulem2  21774  aalioulem3  21775  ulmuni  21832  ulmbdd  21838  ulmdvlem3  21842  mtest  21844  abelthlem8  21879  pilem3  21893  efopn  22078  cxpmul2z  22111  cxpcn3lem  22160  jensen  22357  isppw2  22428  sqf11  22452  mersenne  22541  dchrelbas3  22552  dchrptlem1  22578  dchrpt  22581  lgsval2lem  22620  lgsdchrval  22661  lgsquad3  22675  2sqb  22692  pntrsumbnd2  22791  pntpbnd  22812  pntibnd  22817  istrkgc  22892  istrkgb  22893  tglowdim1i  22929  tgbtwndiff  22934  tgifscgr  22936  tgcgrxfr  22945  lnext  22970  tgbtwnconn1lem3  22977  tgbtwnconn1  22978  legval  22986  legov  22987  legov2  22988  legtrd  22991  legtri3  22992  tglinethru  23012  colline  23020  tglowdim2l  23021  mirreu3  23026  miriso  23039  midexlem  23051  f1otrg  23068  f1otrge  23069  axsegcon  23124  axeuclidlem  23159  axcontlem2  23162  usgra1  23243  usgrares1  23274  nbgraf1olem5  23305  pthdepisspth  23424  iseupa  23537  eupath2  23552  isgrp2d  23673  smcnlem  24043  0lno  24141  ubthlem1  24222  ubthlem3  24224  chocunii  24655  occl  24658  5oalem1  25008  3oalem2  25017  nmopub2tALT  25264  nmfnleub2  25281  lnconi  25388  kbass5  25475  mdslmd1lem1  25680  mdslmd1lem2  25681  cdj1i  25788  disjabrex  25877  disjabrexf  25878  fgreu  25941  xrge0infss  26004  xrofsup  26006  ressprs  26067  xrge0addgt0  26105  submarchi  26154  isarchi3  26155  archiabllem1  26161  archiabllem2a  26162  gsumle  26197  suborng  26234  isarchiofld  26236  pstmxmet  26276  sqsscirc1  26290  ordtrest2NEWlem  26304  ordtconlem1  26306  pnfneige0  26333  lmxrge0  26334  lmdvg  26335  qqhval2  26363  esumcst  26466  esumfsup  26471  esumcvg  26487  sigaclfu2  26516  insiga  26532  measinb  26587  imambfm  26629  oms0  26662  eulerpartlemgvv  26711  dstrvprob  26806  sgnmul  26877  sgnsub  26879  signstfvneq0  26925  afsval  26947  lgambdd  26975  lgamucov  26976  derangenlem  27011  sconpi1  27080  cvmsss2  27115  cvmopnlem  27119  cvmlift3lem7  27166  fprodconst  27440  ifscgr  28026  cgrxfr  28037  btwnconn1lem13  28081  outsideofeu  28113  heicant  28379  mblfinlem1  28381  itg2addnclem  28396  ftc1cnnc  28419  ftc1anclem7  28426  neibastop2lem  28534  sstotbnd2  28626  equivtotbnd  28630  isbnd3  28636  ssbnd  28640  totbndbnd  28641  cntotbnd  28648  heibor1lem  28661  rrncmslem  28684  mzpindd  29035  mzpsubst  29038  mzpcompact2lem  29041  eldioph2b  29054  irrapxlem3  29118  irrapxlem5  29120  pellex  29129  pell1234qrdich  29155  pell14qrexpcl  29161  congabseq  29270  jm2.26a  29302  jm2.26lem3  29303  rmydioph  29316  lnrfg  29428  hbt  29439  fnchoice  29704  cncmpmax  29707  climrec  29729  climsuse  29734  stoweidlem7  29755  stoweidlem34  29782  stoweidlem52  29800  stoweidlem60  29808  wallispilem3  29815  usgra2pthspth  30248  el2spthonot  30342  usg2wotspth  30356  clwwlkf1  30411  Lemma2  30446  frgrancvvdeqlem9  30587  friendshipgt3  30667  lindslinindsimp2  30886  snlindsntor  30894  lincresunit2  30901  islindeps2  30906  4animp1  31088  4an4132  31090  iunconlem2  31558  lssats  32497  lsat0cv  32518  lkrlss  32580  lfl1dim  32606  lfl1dim2N  32607  lkrpssN  32648  hlhgt2  32873  3dim2  32952  2dim  32954  lplncvrlvol  33100  paddasslem11  33314  pmapjat1  33337  2polssN  33399  pclfinclN  33434  pexmidlem8N  33461  lhpexle1lem  33491  4atex  33560  ltrnid  33619  trlator0  33655  cdlemg2cex  34075  tendodi1  34268  tendodi2  34269  diblss  34655  dihopelvalcpre  34733  dihatexv  34823  mapdval4N  35117
  Copyright terms: Public domain W3C validator