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  6039  f1o2ndf1  6445  tz7.49  6693  omabs  6881  omxpenlem  7200  fopwdom  7207  findcard3  7341  frfi  7343  finsschain  7404  marypha1lem  7429  wdomtr  7532  cantnfp1  7626  harcard  7854  numacn  7919  infunsdom1  8082  cofsmo  8138  sornom  8146  ssfin4  8179  fin1a2lem11  8279  fin1a2lem13  8281  ttukeylem5  8382  fpwwe2lem13  8506  pwfseq  8528  00id  9230  addid1  9235  cnegex  9236  negeu  9285  add20  9529  ltmul12a  9855  lediv12a  9892  cru  9981  qextltlem  10777  xleadd1a  10821  xmullem  10832  xlemul1a  10856  ixxss12  10925  ioodisj  11015  seqf1o  11352  mulexpz  11408  leexp1a  11426  faclbnd  11569  abs3lem  12130  cau3lem  12146  rlim3  12280  ello12  12298  lo1bdd2  12306  elo12  12309  rlimconst  12326  isercoll  12449  climcau  12452  climbdd  12453  summolem2  12498  fsumconst  12561  o1fsum  12580  incexclem  12604  bitsfzo  12935  dvdsmulgcd  13042  pc2dvds  13240  pcz  13242  pcadd  13246  pcfac  13256  vdwmc2  13335  vdwlem2  13338  vdwlem10  13346  vdw  13350  ramcl  13385  firest  13648  prdsval  13666  mreexd  13855  mreexexlemd  13857  iscat  13885  cidfval  13889  iscatd2  13894  catcocl  13898  catass  13899  catpropd  13923  cidpropd  13924  moni  13950  monpropd  13951  issubc  14023  subccocl  14030  funcco  14056  funcpropd  14085  fullpropd  14105  nati  14140  natpropd  14161  fucpropd  14162  xpcpropd  14293  curfuncf  14323  curf2ndf  14332  yonffthlem  14367  acsfiindd  14591  mndpropd  14709  mhmeql  14752  isgrpinv  14843  conjnmzb  15028  gass  15066  dfod2  15188  gexdvds  15206  sylow3lem2  15250  efgredlem  15367  efgredeu  15372  oddvdssubg  15458  dprdfcntz  15561  pgpfaclem3  15629  isrng  15656  dvdsrmul1  15746  issubdrg  15881  islmhm2  16102  lmhmeql  16119  lssacsex  16204  issubassa2  16391  opsrval  16523  isphl  16847  cctop  17058  neiptoptop  17183  neiptopreu  17185  tgrest  17211  ordtrest2lem  17255  cnss1  17328  cncnp  17332  isnrm3  17411  uncmp  17454  cmpfi  17459  iuncon  17479  1stcrest  17504  subislly  17532  islly2  17535  cldllycmp  17546  lly1stc  17547  llycmpkgen2  17570  kgencn  17576  xkoccn  17639  ptcnplem  17641  pthaus  17658  txhaus  17667  txkgen  17672  xkohaus  17673  xkococnlem  17679  txcon  17709  regr1lem2  17760  kqreglem1  17761  reghmph  17813  nrmhmph  17814  trfil2  17907  ufileu  17939  flimopn  17995  flimcf  18002  fclscf  18045  ufilcmp  18052  cnpfcf  18061  cnextfun  18083  tgpmulg  18111  symgtgp  18119  tgpt0  18136  divstgplem  18138  ustex2sym  18234  ustex3sym  18235  trust  18247  restutop  18255  restutopopn  18256  ustuqtop2  18260  ustuqtop4  18262  utop3cls  18269  utopreg  18270  cstucnd  18302  ucncn  18303  trcfilu  18312  neipcfilu  18314  ismet2  18351  metequiv2  18528  metcnp  18559  metcnp2  18560  metcnpi3  18564  txmetcnp  18565  metusttoOLD  18575  metustto  18576  metustsymOLD  18579  metustsym  18580  metustOLD  18585  metust  18586  cfilucfilOLD  18587  cfilucfil  18588  metuel2  18597  metutopOLD  18600  psmetutop  18601  restmetu  18605  metucnOLD  18606  metucn  18607  ngptgp  18665  tngngp  18683  nmoleub  18753  icccmp  18844  reconnlem2  18846  reconn  18847  xmetdcn2  18856  metdseq0  18872  metdscn  18874  elcncf2  18908  cncfmet  18926  cnheibor  18968  nmoleub2lem2  19112  nmoleub3  19115  iscfil2  19207  iscfil3  19214  cfilfcls  19215  equivcfil  19240  caubl  19248  bcthlem5  19269  pmltpc  19335  ovollb2  19373  ovoliunnul  19391  ovolicc2lem4  19404  volsup  19438  ioorf  19453  dyadss  19474  dyaddisjlem  19475  mbfposr  19532  cncombf  19538  mbflimsup  19546  i1fmulclem  19582  mbfi1fseqlem4  19598  iblss2  19685  ellimc2  19752  ellimc3  19754  dvnadd  19803  dvmptfsum  19847  dvferm1  19857  dvferm2  19859  fta1g  20078  plyeq0lem  20117  plydivex  20202  fta1  20213  aalioulem2  20238  aalioulem3  20239  ulmuni  20296  ulmbdd  20302  ulmdvlem3  20306  mtest  20308  abelthlem8  20343  pilem3  20357  efopn  20537  cxpmul2z  20570  cxpcn3lem  20619  jensen  20815  isppw2  20886  sqf11  20910  mersenne  20999  dchrelbas3  21010  dchrptlem1  21036  dchrpt  21039  lgsval2lem  21078  lgsdchrval  21119  lgsquad3  21133  2sqb  21150  pntrsumbnd2  21249  pntpbnd  21270  pntibnd  21275  usgra1  21381  usgrares1  21412  nbgraf1olem5  21443  pthdepisspth  21562  iseupa  21675  eupath2  21690  isgrp2d  21811  smcnlem  22181  0lno  22279  ubthlem1  22360  ubthlem3  22362  chocunii  22791  occl  22794  5oalem1  23144  3oalem2  23153  nmopub2tALT  23400  nmfnleub2  23417  lnconi  23524  kbass5  23611  mdslmd1lem1  23816  mdslmd1lem2  23817  cdj1i  23924  disjabrex  24012  disjabrexf  24013  xrofsup  24114  xrge0addgt0  24202  subofld  24233  pstmxmet  24280  sqsscirc1  24294  pnfneige0  24324  lmxrge0  24325  lmdvg  24326  qqhval2  24354  esumcst  24443  esumfsup  24448  esumcvg  24464  sigaclfu2  24492  insiga  24508  measinb  24563  imambfm  24600  dstrvprob  24717  lgambdd  24809  lgamucov  24810  derangenlem  24845  sconpi1  24914  cvmsss2  24949  cvmopnlem  24953  cvmlift3lem7  25000  fprodconst  25291  axsegcon  25814  axeuclidlem  25849  axcontlem2  25852  ifscgr  25926  cgrxfr  25937  btwnconn1lem13  25981  outsideofeu  26013  mblfinlem  26190  itg2addnclem  26202  ftc1cnnc  26225  neibastop2lem  26326  sstotbnd2  26420  equivtotbnd  26424  isbnd3  26430  ssbnd  26434  totbndbnd  26435  cntotbnd  26442  heibor1lem  26455  rrncmslem  26478  mzpindd  26740  mzpsubst  26742  mzpcompact2lem  26745  eldioph2b  26758  irrapxlem3  26824  irrapxlem5  26826  pellex  26835  pell1234qrdich  26861  pell14qrexpcl  26867  congabseq  26976  jm2.26a  27008  jm2.26lem3  27009  rmydioph  27022  uvcf1  27156  lindfmm  27212  lnrfg  27238  hbt  27249  fnchoice  27614  cncmpmax  27617  climrec  27643  climsuse  27648  stoweidlem7  27670  stoweidlem34  27697  stoweidlem52  27715  stoweidlem60  27723  wallispilem3  27730  swrdswrdlem  28085  shwrdeqrep  28160  usgra2pthspth  28179  el2spthonot  28211  usg2wotspth  28225  frgrancvvdeqlem9  28288  iunconlem2  28902  lssats  29649  lsat0cv  29670  lkrlss  29732  lfl1dim  29758  lfl1dim2N  29759  lkrpssN  29800  hlhgt2  30025  3dim2  30104  2dim  30106  lplncvrlvol  30252  paddasslem11  30466  pmapjat1  30489  2polssN  30551  pclfinclN  30586  pexmidlem8N  30613  lhpexle1lem  30643  4atex  30712  ltrnid  30771  trlator0  30807  cdlemg2cex  31227  tendodi1  31420  tendodi2  31421  diblss  31807  dihopelvalcpre  31885  dihatexv  31975  mapdval4N  32269
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