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  5987  tz7.49  6638  omabs  6826  omxpenlem  7145  fopwdom  7152  findcard3  7286  frfi  7288  finsschain  7348  marypha1lem  7373  wdomtr  7476  cantnfp1  7570  harcard  7798  numacn  7863  infunsdom1  8026  cofsmo  8082  sornom  8090  ssfin4  8123  fin1a2lem11  8223  fin1a2lem13  8225  ttukeylem5  8326  fpwwe2lem13  8450  pwfseq  8472  00id  9173  addid1  9178  cnegex  9179  negeu  9228  add20  9472  ltmul12a  9798  lediv12a  9835  cru  9924  qextltlem  10720  xleadd1a  10764  xmullem  10775  xlemul1a  10799  ixxss12  10868  ioodisj  10958  seqf1o  11291  mulexpz  11347  leexp1a  11365  faclbnd  11508  abs3lem  12069  cau3lem  12085  rlim3  12219  ello12  12237  lo1bdd2  12245  elo12  12248  rlimconst  12265  isercoll  12388  climcau  12391  climbdd  12392  summolem2  12437  fsumconst  12500  o1fsum  12519  incexclem  12543  bitsfzo  12874  dvdsmulgcd  12981  pc2dvds  13179  pcz  13181  pcadd  13185  pcfac  13195  vdwmc2  13274  vdwlem2  13277  vdwlem10  13285  vdw  13289  ramcl  13324  firest  13587  prdsval  13605  mreexd  13794  mreexexlemd  13796  iscat  13824  cidfval  13828  iscatd2  13833  catcocl  13837  catass  13838  catpropd  13862  cidpropd  13863  moni  13889  monpropd  13890  issubc  13962  subccocl  13969  funcco  13995  funcpropd  14024  fullpropd  14044  nati  14079  natpropd  14100  fucpropd  14101  xpcpropd  14232  curfuncf  14262  curf2ndf  14271  yonffthlem  14306  acsfiindd  14530  mndpropd  14648  mhmeql  14691  isgrpinv  14782  conjnmzb  14967  gass  15005  dfod2  15127  gexdvds  15145  sylow3lem2  15189  efgredlem  15306  efgredeu  15311  oddvdssubg  15397  dprdfcntz  15500  pgpfaclem3  15568  isrng  15595  dvdsrmul1  15685  issubdrg  15820  islmhm2  16041  lmhmeql  16058  lssacsex  16143  issubassa2  16330  opsrval  16462  isphl  16782  cctop  16993  neiptoptop  17118  neiptopreu  17120  tgrest  17145  ordtrest2lem  17189  cnss1  17262  cncnp  17266  isnrm3  17345  uncmp  17388  cmpfi  17393  iuncon  17412  1stcrest  17437  subislly  17465  islly2  17468  cldllycmp  17479  lly1stc  17480  llycmpkgen2  17503  kgencn  17509  xkoccn  17572  ptcnplem  17574  pthaus  17591  txhaus  17600  txkgen  17605  xkohaus  17606  xkococnlem  17612  txcon  17642  regr1lem2  17693  kqreglem1  17694  reghmph  17746  nrmhmph  17747  trfil2  17840  ufileu  17872  flimopn  17928  flimcf  17935  fclscf  17978  ufilcmp  17985  cnpfcf  17994  cnextfun  18016  tgpmulg  18044  symgtgp  18052  tgpt0  18069  divstgplem  18071  ustex2sym  18167  ustex3sym  18168  trust  18180  restutop  18188  restutopopn  18189  ustuqtop2  18193  ustuqtop4  18195  utop3cls  18202  utopreg  18203  cstucnd  18235  ucncn  18236  trcfilu  18245  neipcfilu  18247  ismet2  18272  metequiv2  18430  metcnp  18461  metcnp2  18462  metcnpi3  18466  txmetcnp  18467  metustto  18473  metustsym  18475  metust  18478  cfilucfil  18479  metuel2  18485  metutop  18487  restmetu  18489  metucn  18490  ngptgp  18548  tngngp  18566  nmoleub  18636  icccmp  18727  reconnlem2  18729  reconn  18730  xmetdcn2  18739  metdseq0  18755  metdscn  18757  elcncf2  18791  cncfmet  18809  cnheibor  18851  nmoleub2lem2  18995  nmoleub3  18998  iscfil2  19090  iscfil3  19097  cfilfcls  19098  equivcfil  19123  caubl  19131  bcthlem5  19150  pmltpc  19214  ovollb2  19252  ovoliunnul  19270  ovolicc2lem4  19283  volsup  19317  ioorf  19332  dyadss  19353  dyaddisjlem  19354  mbfposr  19411  cncombf  19417  mbflimsup  19425  i1fmulclem  19461  mbfi1fseqlem4  19477  iblss2  19564  ellimc2  19631  ellimc3  19633  dvnadd  19682  dvmptfsum  19726  dvferm1  19736  dvferm2  19738  fta1g  19957  plyeq0lem  19996  plydivex  20081  fta1  20092  aalioulem2  20117  aalioulem3  20118  ulmuni  20175  ulmbdd  20181  ulmdvlem3  20185  mtest  20187  abelthlem8  20222  pilem3  20236  efopn  20416  cxpmul2z  20449  cxpcn3lem  20498  jensen  20694  isppw2  20765  sqf11  20789  mersenne  20878  dchrelbas3  20889  dchrptlem1  20915  dchrpt  20918  lgsval2lem  20957  lgsdchrval  20998  lgsquad3  21012  2sqb  21029  pntrsumbnd2  21128  pntpbnd  21149  pntibnd  21154  usgra1  21260  usgrares1  21290  nbgraf1olem5  21321  pthdepisspth  21428  iseupa  21535  eupath2  21550  isgrp2d  21671  smcnlem  22041  0lno  22139  ubthlem1  22220  ubthlem3  22222  chocunii  22651  occl  22654  5oalem1  23004  3oalem2  23013  nmopub2tALT  23260  nmfnleub2  23277  lnconi  23384  kbass5  23471  mdslmd1lem1  23676  mdslmd1lem2  23677  cdj1i  23784  disjabrex  23868  disjabrexf  23869  xrofsup  23962  xrge0addgt0  24043  subofld  24071  sqsscirc1  24110  pnfneige0  24140  lmxrge0  24141  lmdvg  24142  qqhval2  24165  esumcst  24251  esumfsup  24256  esumcvg  24272  sigaclfu2  24300  insiga  24316  measinb  24369  imambfm  24406  dstrvprob  24508  lgambdd  24600  lgamucov  24601  derangenlem  24636  sconpi1  24705  cvmsss2  24740  cvmopnlem  24744  cvmlift3lem7  24791  fprodconst  25081  axsegcon  25580  axeuclidlem  25615  axcontlem2  25618  ifscgr  25692  cgrxfr  25703  btwnconn1lem13  25747  outsideofeu  25779  itg2addnclem  25957  ftc1cnnc  25979  neibastop2lem  26080  sstotbnd2  26174  equivtotbnd  26178  isbnd3  26184  ssbnd  26188  totbndbnd  26189  cntotbnd  26196  heibor1lem  26209  rrncmslem  26232  mzpindd  26494  mzpsubst  26496  mzpcompact2lem  26499  eldioph2b  26512  irrapxlem3  26578  irrapxlem5  26580  pellex  26589  pell1234qrdich  26615  pell14qrexpcl  26621  congabseq  26730  jm2.26a  26762  jm2.26lem3  26763  rmydioph  26776  uvcf1  26910  lindfmm  26966  lnrfg  26992  hbt  27003  fnchoice  27368  cncmpmax  27371  climrec  27397  climsuse  27402  stoweidlem7  27424  stoweidlem34  27451  stoweidlem52  27469  stoweidlem60  27477  wallispilem3  27484  frgrancvvdeqlem9  27793  lssats  29127  lsat0cv  29148  lkrlss  29210  lfl1dim  29236  lfl1dim2N  29237  lkrpssN  29278  hlhgt2  29503  3dim2  29582  2dim  29584  lplncvrlvol  29730  paddasslem11  29944  pmapjat1  29967  2polssN  30029  pclfinclN  30064  pexmidlem8N  30091  lhpexle1lem  30121  4atex  30190  ltrnid  30249  trlator0  30285  cdlemg2cex  30705  tendodi1  30898  tendodi2  30899  diblss  31285  dihopelvalcpre  31363  dihatexv  31453  mapdval4N  31747
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